[STATEMENT]
lemma unwind_cont_\<Delta>3: "unwind_cont \<Delta>3 {\<Delta>3,\<Delta>4,\<Delta>e}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unwind_cont \<Delta>3 {\<Delta>3, \<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>3 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1"
[PROOF STATE]
proof (state)
this:
reachNT s
reach s1
\<Delta>3 s vl s1 vl1

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>3 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1
[PROOF STEP]
obtain CID uid ul ul1 wl where uuid: "isREVNth s uid PID N"
  and rs: "reach s" and ph: "phase s CID = revPH" (is "?ph = _")  and ss1: "eqExcPID_N s s1"
  and PID: "PID \<in>\<in> paperIDs s CID" and B: "B vl vl1"
  and vlvl1: "vl \<noteq> []" "vl1 \<noteq> []"
  and vl_wl: "vl = (map (Pair revPH) ul) @ (map (Pair disPH) wl)"
  and vl1_wl: "vl1 = (map (Pair revPH) ul1) @ (map (Pair disPH) wl)"
  and ulul1: "ul \<noteq> [] \<and> ul1 \<noteq> [] \<and> last ul = last ul1"
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
\<Delta>3 s vl s1 vl1

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

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

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

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>3 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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
phase s CID = revPH
eqExcPID_N s s1
PID \<in>\<in> paperIDs s CID
B vl vl1
vl \<noteq> []
vl1 \<noteq> []
vl = map (Pair revPH) ul @ map (Pair disPH) wl
vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl
ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1

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>3 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
have ph1: "phase s1 CID = revPH"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phase s1 CID = revPH
[PROOF STEP]
using ss1 ph eqExcPID_N_imp
[PROOF STATE]
proof (prove)
using this:
eqExcPID_N s s1
phase s CID = revPH
eqExcPID_N ?s ?s1.0 \<Longrightarrow> confIDs ?s = confIDs ?s1.0 \<and> conf ?s = conf ?s1.0 \<and> userIDs ?s = userIDs ?s1.0 \<and> pass ?s = pass ?s1.0 \<and> user ?s = user ?s1.0 \<and> roles ?s = roles ?s1.0 \<and> paperIDs ?s = paperIDs ?s1.0 \<and> eeqExcPID_N (paper ?s) (paper ?s1.0) \<and> pref ?s = pref ?s1.0 \<and> voronkov ?s = voronkov ?s1.0 \<and> news ?s = news ?s1.0 \<and> phase ?s = phase ?s1.0 \<and> getAllPaperIDs ?s = getAllPaperIDs ?s1.0 \<and> isRev ?s ?cid ?uid ?pid = isRev ?s1.0 ?cid ?uid ?pid \<and> getReviewIndex ?s ?cid ?uid ?pid = getReviewIndex ?s1.0 ?cid ?uid ?pid \<and> getRevRole ?s ?cid ?uid ?pid = getRevRole ?s1.0 ?cid ?uid ?pid \<and> length (reviewsPaper (paper ?s ?pid)) = length (reviewsPaper (paper ?s1.0 ?pid))

goal (1 subgoal):
 1. phase s1 CID = revPH
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
phase s1 CID = revPH

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>3 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
from ulul1
[PROOF STATE]
proof (chain)
picking this:
ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1
[PROOF STEP]
obtain u ul' u1 ul1' where ul: "ul = u # ul'" and ul1: "ul1 = u1 # ul1'"
[PROOF STATE]
proof (prove)
using this:
ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1

goal (1 subgoal):
 1. (\<And>u ul' u1 ul1'. \<lbrakk>ul = u # ul'; ul1 = u1 # ul1'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis list.exhaust)
[PROOF STATE]
proof (state)
this:
ul = u # ul'
ul1 = u1 # ul1'

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>3 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
obtain vl' vl1' where
  vl:  "vl = (revPH, u) # vl'"    and vl'_wl: "vl' = (map (Pair revPH) ul') @ (map (Pair disPH) wl)" and
  vl1: "vl1 = (revPH, u1) # vl1'" and vl1'_wl: "vl1' = (map (Pair revPH) ul1') @ (map (Pair disPH) wl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>vl' vl1'. \<lbrakk>vl = (revPH, u) # vl'; vl' = map (Pair revPH) ul' @ map (Pair disPH) wl; vl1 = (revPH, u1) # vl1'; vl1' = map (Pair revPH) ul1' @ map (Pair disPH) wl\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding vl_wl ul vl1_wl ul1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>vl' vl1'. \<lbrakk>map (Pair revPH) (u # ul') @ map (Pair disPH) wl = (revPH, u) # vl'; vl' = map (Pair revPH) ul' @ map (Pair disPH) wl; map (Pair revPH) (u1 # ul1') @ map (Pair disPH) wl = (revPH, u1) # vl1'; vl1' = map (Pair revPH) ul1' @ map (Pair disPH) wl\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vl = (revPH, u) # vl'
vl' = map (Pair revPH) ul' @ map (Pair disPH) wl
vl1 = (revPH, u1) # vl1'
vl1' = map (Pair revPH) ul1' @ map (Pair disPH) wl

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>3 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
have uid_notin: "uid \<notin> UIDs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uid \<notin> UIDs
[PROOF STEP]
using uid
[PROOF STATE]
proof (prove)
using this:
isRevNth s CID uid PID N

goal (1 subgoal):
 1. uid \<notin> UIDs
[PROOF STEP]
by (metis reachNT_non_isRevNth rsT)
[PROOF STATE]
proof (state)
this:
uid \<notin> UIDs

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>3 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
proof(cases "ul1' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
ul1' \<noteq> emptyReview

goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
note ul1' = False
[PROOF STATE]
proof (state)
this:
ul1' \<noteq> emptyReview

goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
hence ul_ul1': "last ul = last ul1'"
[PROOF STATE]
proof (prove)
using this:
ul1' \<noteq> emptyReview

goal (1 subgoal):
 1. last ul = last ul1'
[PROOF STEP]
using ulul1
[PROOF STATE]
proof (prove)
using this:
ul1' \<noteq> emptyReview
ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1

goal (1 subgoal):
 1. last ul = last ul1'
[PROOF STEP]
unfolding ul1
[PROOF STATE]
proof (prove)
using this:
ul1' \<noteq> emptyReview
ul \<noteq> emptyReview \<and> u1 # ul1' \<noteq> emptyReview \<and> last ul = last (u1 # ul1')

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

goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
have uid1: "isRevNth s1 CID uid PID N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isRevNth s1 CID uid PID N
[PROOF STEP]
using ss1 uid
[PROOF STATE]
proof (prove)
using this:
eqExcPID_N s s1
isRevNth s CID uid PID N

goal (1 subgoal):
 1. isRevNth s1 CID uid PID N
[PROOF STEP]
unfolding eqExcPID_N_def
[PROOF STATE]
proof (prove)
using this:
confIDs s = confIDs s1 \<and> conf s = conf s1 \<and> userIDs s = userIDs s1 \<and> pass s = pass s1 \<and> user s = user s1 \<and> roles s = roles s1 \<and> paperIDs s = paperIDs s1 \<and> eeqExcPID_N (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1
isRevNth s CID uid PID N

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

goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
define a1 where "a1 \<equiv> Uact (uReview CID uid (pass s uid) PID N u1)"
[PROOF STATE]
proof (state)
this:
a1 \<equiv> Uact (uReview CID uid (pass s uid) PID N u1)

goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
obtain s1' ou1 where step1: "step s1 a1 = (ou1,s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ou1 s1'. step s1 a1 = (ou1, s1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod.exhaust)
[PROOF STATE]
proof (state)
this:
step s1 a1 = (ou1, s1')

goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
let ?trn1 = "Trans s1 a1 ou1 s1'"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
have s1s1': "eqExcPID_N s1 s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID_N s1 s1'
[PROOF STEP]
using a1_def step1
[PROOF STATE]
proof (prove)
using this:
a1 \<equiv> Uact (uReview CID uid (pass s uid) PID N u1)
step s1 a1 = (ou1, s1')

goal (1 subgoal):
 1. eqExcPID_N s1 s1'
[PROOF STEP]
by (metis uReview_uuReview_step_eqExcPID_N)
[PROOF STATE]
proof (state)
this:
eqExcPID_N s1 s1'

goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
have ss1': "eqExcPID_N s s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID_N s s1'
[PROOF STEP]
using eqExcPID_N_trans[OF ss1 s1s1']
[PROOF STATE]
proof (prove)
using this:
eqExcPID_N s s1'

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

goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
hence many_s1': "PID \<in>\<in> paperIDs s1' CID" "isRevNth s1' CID uid PID N"
    "phase s1' CID = revPH" "pass s1' uid = pass s uid"
[PROOF STATE]
proof (prove)
using this:
eqExcPID_N s s1'

goal (1 subgoal):
 1. (PID \<in>\<in> paperIDs s1' CID &&& isRevNth s1' CID uid PID N) &&& phase s1' CID = revPH &&& pass s1' uid = pass s uid
[PROOF STEP]
using uid PID ph
[PROOF STATE]
proof (prove)
using this:
eqExcPID_N s s1'
isRevNth s CID uid PID N
PID \<in>\<in> paperIDs s CID
phase s CID = revPH

goal (1 subgoal):
 1. (PID \<in>\<in> paperIDs s1' CID &&& isRevNth s1' CID uid PID N) &&& phase s1' CID = revPH &&& pass s1' uid = pass s uid
[PROOF STEP]
unfolding eqExcPID_N_def
[PROOF STATE]
proof (prove)
using this:
confIDs s = confIDs s1' \<and> conf s = conf s1' \<and> userIDs s = userIDs s1' \<and> pass s = pass s1' \<and> user s = user s1' \<and> roles s = roles s1' \<and> paperIDs s = paperIDs s1' \<and> eeqExcPID_N (paper s) (paper s1') \<and> pref s = pref s1' \<and> voronkov s = voronkov s1' \<and> news s = news s1' \<and> phase s = phase s1'
isRevNth s CID uid PID N
PID \<in>\<in> paperIDs s CID
phase s CID = revPH

goal (1 subgoal):
 1. (PID \<in>\<in> paperIDs s1' CID &&& isRevNth s1' CID uid PID N) &&& phase s1' CID = revPH &&& pass s1' uid = pass s uid
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
PID \<in>\<in> paperIDs s1' CID
isRevNth s1' CID uid PID N
phase s1' CID = revPH
pass s1' uid = pass s uid

goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
hence more_s1': "uid \<in>\<in> userIDs s1'" "CID \<in>\<in> confIDs s1'"
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> paperIDs s1' CID
isRevNth s1' CID uid PID N
phase s1' CID = revPH
pass s1' uid = pass s uid

goal (1 subgoal):
 1. uid \<in>\<in> userIDs s1' &&& CID \<in>\<in> confIDs s1'
[PROOF STEP]
by (metis paperIDs_confIDs reach_PairI roles_userIDs rs1 step1 many_s1'(1))+
[PROOF STATE]
proof (state)
this:
uid \<in>\<in> userIDs s1'
CID \<in>\<in> confIDs s1'

goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
have f: "f ?trn1 = (revPH,u1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Trans s1 a1 ou1 s1') = (revPH, u1)
[PROOF STEP]
unfolding a1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Trans s1 (Uact (uReview CID uid (pass s uid) PID N u1)) ou1 s1') = (revPH, u1)
[PROOF STEP]
using ph1
[PROOF STATE]
proof (prove)
using this:
phase s1 CID = revPH

goal (1 subgoal):
 1. f (Trans s1 (Uact (uReview CID uid (pass s uid) PID N u1)) ou1 s1') = (revPH, u1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (Trans s1 a1 ou1 s1') = (revPH, u1)

goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
have rs1': "reach s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach s1'
[PROOF STEP]
using rs1 step1
[PROOF STATE]
proof (prove)
using this:
reach s1
step s1 a1 = (ou1, s1')

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

goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
have ou1: "ou1 = outOK"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ou1 = outOK
[PROOF STEP]
using step1 uid1 ph
[PROOF STATE]
proof (prove)
using this:
step s1 a1 = (ou1, s1')
isRevNth s1 CID uid PID N
phase s CID = revPH

goal (1 subgoal):
 1. ou1 = outOK
[PROOF STEP]
unfolding a1_def
[PROOF STATE]
proof (prove)
using this:
step s1 (Uact (uReview CID uid (pass s uid) PID N u1)) = (ou1, s1')
isRevNth s1 CID uid PID N
phase s CID = revPH

goal (1 subgoal):
 1. ou1 = outOK
[PROOF STEP]
apply (auto simp add: u_defs many_s1' more_s1')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>phase s CID = revPH; s1 = s1'; ou1 = outErr; \<not> isRev s1' CID uid PID\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>phase s CID = revPH; s1 = s1'; ou1 = outErr; getReviewIndex s1' CID uid PID \<noteq> N\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis isRevNth_getReviewIndex isRev_def3 many_s1'(2) rs1')+
[PROOF STATE]
proof (state)
this:
ou1 = outOK

goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
have ?iact
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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 (5 subgoals):
 1. step s1 ?a1.0 = (?ou1.0, ?s1')
 2. \<phi> (Trans s1 ?a1.0 ?ou1.0 ?s1')
 3. consume (Trans s1 ?a1.0 ?ou1.0 ?s1') vl1 ?vl1'
 4. \<not> \<gamma> (Trans s1 ?a1.0 ?ou1.0 ?s1')
 5. \<Delta>3 s vl ?s1' ?vl1' \<or> \<Delta>4 s vl ?s1' ?vl1' \<or> \<Delta>e s vl ?s1' ?vl1'
[PROOF STEP]
show "step s1 a1 = (ou1,s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step s1 a1 = (ou1, s1')
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
step s1 a1 = (ou1, s1')

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

goal (1 subgoal):
 1. \<phi> (Trans s1 a1 ou1 s1')
[PROOF STEP]
unfolding a1_def
[PROOF STATE]
proof (prove)
using this:
ou1 = outOK

goal (1 subgoal):
 1. \<phi> (Trans s1 (Uact (uReview CID uid (pass s uid) PID N u1)) ou1 s1')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s1 a1 ou1 s1')

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

goal (1 subgoal):
 1. consume (Trans s1 a1 ou1 s1') vl1 vl1'
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 a1 ou1 s1')
f (Trans s1 a1 ou1 s1') = (revPH, u1)

goal (1 subgoal):
 1. consume (Trans s1 a1 ou1 s1') vl1 vl1'
[PROOF STEP]
unfolding consume_def vl1 ul1
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 a1 ou1 s1')
f (Trans s1 a1 ou1 s1') = (revPH, u1)

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

goal (2 subgoals):
 1. \<not> \<gamma> (Trans s1 a1 ou1 s1')
 2. \<Delta>3 s vl s1' vl1' \<or> \<Delta>4 s vl s1' vl1' \<or> \<Delta>e s vl s1' vl1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> \<gamma> (Trans s1 a1 ou1 s1')
 2. \<Delta>3 s vl s1' vl1' \<or> \<Delta>4 s vl s1' vl1' \<or> \<Delta>e s vl s1' vl1'
[PROOF STEP]
show "\<not> \<gamma> ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<gamma> (Trans s1 a1 ou1 s1')
[PROOF STEP]
by (simp add: a1_def uid_notin)
[PROOF STATE]
proof (state)
this:
\<not> \<gamma> (Trans s1 a1 ou1 s1')

goal (1 subgoal):
 1. \<Delta>3 s vl s1' vl1' \<or> \<Delta>4 s vl s1' vl1' \<or> \<Delta>e s vl s1' vl1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>3 s vl s1' vl1' \<or> \<Delta>4 s vl s1' vl1' \<or> \<Delta>e s vl s1' vl1'
[PROOF STEP]
have "\<Delta>3 s vl s1' vl1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>3 s vl s1' vl1'
[PROOF STEP]
unfolding \<Delta>3_def B_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>cid uid. PID \<in>\<in> paperIDs s cid \<and> phase s cid = revPH \<and> isREVNth s uid PID N \<and> eqExcPID_N s s1' \<and> (\<exists>ul ul1 wl. vl = map (Pair revPH) ul @ map (Pair disPH) wl \<and> vl1' = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1)
[PROOF STEP]
using ph PID ss1' uuid ul1' vl_wl vl1'_wl ulul1 ul_ul1'
[PROOF STATE]
proof (prove)
using this:
phase s CID = revPH
PID \<in>\<in> paperIDs s CID
eqExcPID_N s s1'
isREVNth s uid PID N
ul1' \<noteq> emptyReview
vl = map (Pair revPH) ul @ map (Pair disPH) wl
vl1' = map (Pair revPH) ul1' @ map (Pair disPH) wl
ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1
last ul = last ul1'

goal (1 subgoal):
 1. \<exists>cid uid. PID \<in>\<in> paperIDs s cid \<and> phase s cid = revPH \<and> isREVNth s uid PID N \<and> eqExcPID_N s s1' \<and> (\<exists>ul ul1 wl. vl = map (Pair revPH) ul @ map (Pair disPH) wl \<and> vl1' = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<Delta>3 s vl s1' vl1'

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

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

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

goal (2 subgoals):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
 2. ul1' \<noteq> emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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:
iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1

goal (1 subgoal):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ul1' = emptyReview

goal (1 subgoal):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
hence ul1: "ul1 = [u1]"
[PROOF STATE]
proof (prove)
using this:
ul1' = emptyReview

goal (1 subgoal):
 1. ul1 = u1 # emptyReview
[PROOF STEP]
unfolding ul1
[PROOF STATE]
proof (prove)
using this:
ul1' = emptyReview

goal (1 subgoal):
 1. u1 # ul1' = u1 # emptyReview
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ul1 = u1 # emptyReview

goal (1 subgoal):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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 vll'
[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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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 vll'"
[PROOF STATE]
proof (state)
this:
step s a = (ou, s')
\<not> T (Trans s a ou s')
consume (Trans s a ou s') vl vll'

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

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

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

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

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

goal (2 subgoals):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
 2. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
obtain ou1 and s1' where step1: "step s1 a = (ou1,s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ou1 s1'. step s1 a = (ou1, s1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod.exhaust)
[PROOF STATE]
proof (state)
this:
step s1 a = (ou1, s1')

goal (2 subgoals):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
 2. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
let ?trn1 = "Trans s1 a ou1 s1'"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
 2. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
have s's1': "eqExcPID_N s' s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID_N s' s1'
[PROOF STEP]
using eqExcPID_N_step[OF ss1 step step1]
[PROOF STATE]
proof (prove)
using this:
eqExcPID_N s' s1'

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

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

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

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

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

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

goal (4 subgoals):
 1. consume (Trans s1 a ou1 s1') vl1 ?vl1'
 2. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
 3. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 4. \<Delta>3 s' vll' s1' ?vl1' \<or> \<Delta>4 s' vll' s1' ?vl1' \<or> \<Delta>e s' vll' s1' ?vl1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. consume (Trans s1 a ou1 s1') vl1 ?vl1'
 2. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
 3. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 4. \<Delta>3 s' vll' s1' ?vl1' \<or> \<Delta>4 s' vll' s1' ?vl1' \<or> \<Delta>e s' vll' s1' ?vl1'
[PROOF STEP]
show "consume ?trn1 vl1 vl1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consume (Trans s1 a ou1 s1') vl1 vl1
[PROOF STEP]
unfolding consume_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. if \<phi> (Trans s1 a ou1 s1') then vl1 \<noteq> [] \<and> f (Trans s1 a ou1 s1') = hd vl1 \<and> vl1 = tl vl1 else vl1 = vl1
[PROOF STEP]
using \<phi>1
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s1 a ou1 s1')

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

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

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

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

goal (1 subgoal):
 1. g (Trans s a ou s') = g (Trans s1 a ou1 s1')
[PROOF STEP]
using eqExcPID_N_step_out[OF ss1 step step1 rsT rs1 PID ph]
[PROOF STATE]
proof (prove)
using this:
\<gamma> (Trans s a ou s')
userOfA a \<in> UIDs \<Longrightarrow> ou = ou1

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

goal (1 subgoal):
 1. \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
[PROOF STEP]
show "?\<Delta> s' vll' s1' vl1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
[PROOF STEP]
proof(cases "?ph' = revPH")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. phase s' CID = revPH \<Longrightarrow> \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
 2. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
phase s' CID = revPH

goal (2 subgoals):
 1. phase s' CID = revPH \<Longrightarrow> \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
 2. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
[PROOF STEP]
hence "\<Delta>3 s' vll' s1' vl1"
[PROOF STATE]
proof (prove)
using this:
phase s' CID = revPH

goal (1 subgoal):
 1. \<Delta>3 s' vll' s1' vl1
[PROOF STEP]
unfolding \<Delta>3_def B_def vll'
[PROOF STATE]
proof (prove)
using this:
phase s' CID = revPH

goal (1 subgoal):
 1. \<exists>cid uid. PID \<in>\<in> paperIDs s' cid \<and> phase s' cid = revPH \<and> isREVNth s' uid PID N \<and> eqExcPID_N s' s1' \<and> (\<exists>ul ul1 wl. vl = map (Pair revPH) ul @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1)
[PROOF STEP]
using ph PID s's1' PID' uuid' vl_wl vl1_wl ulul1
[PROOF STATE]
proof (prove)
using this:
phase s' CID = revPH
phase s CID = revPH
PID \<in>\<in> paperIDs s CID
eqExcPID_N s' s1'
PID \<in>\<in> paperIDs s' CID
isREVNth s' uid PID N
vl = map (Pair revPH) ul @ map (Pair disPH) wl
vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl
ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1

goal (1 subgoal):
 1. \<exists>cid uid. PID \<in>\<in> paperIDs s' cid \<and> phase s' cid = revPH \<and> isREVNth s' uid PID N \<and> eqExcPID_N s' s1' \<and> (\<exists>ul ul1 wl. vl = map (Pair revPH) ul @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<Delta>3 s' vll' s1' vl1

goal (2 subgoals):
 1. phase s' CID = revPH \<Longrightarrow> \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
 2. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Delta>3 s' vll' s1' vl1

goal (1 subgoal):
 1. \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1

goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
phase s' CID \<noteq> revPH

goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
[PROOF STEP]
hence "?ph' > revPH"
[PROOF STATE]
proof (prove)
using this:
phase s' CID \<noteq> revPH

goal (1 subgoal):
 1. revPH < phase s' CID
[PROOF STEP]
using ph rs step
[PROOF STATE]
proof (prove)
using this:
phase s' CID \<noteq> revPH
phase s CID = revPH
reach s
step s a = (ou, s')

goal (1 subgoal):
 1. revPH < phase s' CID
[PROOF STEP]
by (metis le_less phase_increases2 snd_conv)
[PROOF STATE]
proof (state)
this:
revPH < phase s' CID

goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
[PROOF STEP]
hence "\<Delta>e s' vll' s1' vl1"
[PROOF STATE]
proof (prove)
using this:
revPH < phase s' CID

goal (1 subgoal):
 1. \<Delta>e s' vll' s1' vl1
[PROOF STEP]
using vlvl1 PID'
[PROOF STATE]
proof (prove)
using this:
revPH < phase s' CID
vl \<noteq> []
vl1 \<noteq> []
PID \<in>\<in> paperIDs s' CID

goal (1 subgoal):
 1. \<Delta>e s' vll' s1' vl1
[PROOF STEP]
unfolding \<Delta>e_def vll' vl_wl ul
[PROOF STATE]
proof (prove)
using this:
revPH < phase s' CID
map (Pair revPH) (u # ul') @ map (Pair disPH) wl \<noteq> []
vl1 \<noteq> []
PID \<in>\<in> paperIDs s' CID

goal (1 subgoal):
 1. map (Pair revPH) (u # ul') @ map (Pair disPH) wl \<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 (map (Pair revPH) (u # ul') @ map (Pair disPH) wl)) = revPH))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>e s' vll' s1' vl1

goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Delta>e s' vll' s1' vl1

goal (1 subgoal):
 1. \<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Delta>3 s' vll' s1' vl1 \<or> \<Delta>4 s' vll' s1' vl1 \<or> \<Delta>e s' vll' s1' vl1

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
obtain cid uid' p rc
        where "a = Uact (uReview cid uid' p PID N rc) \<or>
               a = UUact (uuReview cid uid' p PID N rc)" and ou: "ou = outOK"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>cid uid' p rc. \<lbrakk>a = Uact (uReview cid uid' p PID N rc) \<or> a = UUact (uuReview cid uid' p PID N rc); ou = outOK\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<phi> c ph step ph
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')
consume (Trans s a ou s') vl vll'
phase s CID = revPH
step s a = (ou, s')
phase s CID = revPH

goal (1 subgoal):
 1. (\<And>cid uid' p rc. \<lbrakk>a = Uact (uReview cid uid' p PID N rc) \<or> a = UUact (uuReview cid uid' p PID N rc); ou = outOK\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding vl consume_def \<phi>_def2 vll'
[PROOF STATE]
proof (prove)
using this:
ou = outOK \<and> (\<exists>cid uid p rc. a = Uact (uReview cid uid p PID N rc) \<or> a = UUact (uuReview cid uid p PID N rc))
if ou = outOK \<and> (\<exists>cid uid p rc. a = Uact (uReview cid uid p PID N rc) \<or> a = UUact (uuReview cid uid p PID N rc)) then (revPH, u) # vl' \<noteq> [] \<and> f (Trans s a ou s') = hd ((revPH, u) # vl') \<and> vl' = tl ((revPH, u) # vl') else vl' = (revPH, u) # vl'
phase s CID = revPH
step s a = (ou, s')
phase s CID = revPH

goal (1 subgoal):
 1. (\<And>cid uid' p rc. \<lbrakk>a = Uact (uReview cid uid' p PID N rc) \<or> a = UUact (uuReview cid uid' p PID N rc); ou = outOK\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
a = Uact (uReview cid uid' p PID N rc) \<or> a = UUact (uuReview cid uid' p PID N rc)
ou = outOK

goal (1 subgoal):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
hence a: "a = Uact (uReview cid uid' p PID N rc)"
[PROOF STATE]
proof (prove)
using this:
a = Uact (uReview cid uid' p PID N rc) \<or> a = UUact (uuReview cid uid' p PID N rc)
ou = outOK

goal (1 subgoal):
 1. a = Uact (uReview cid uid' p PID N rc)
[PROOF STEP]
using step ph
[PROOF STATE]
proof (prove)
using this:
a = Uact (uReview cid uid' p PID N rc) \<or> a = UUact (uuReview cid uid' p PID N rc)
ou = outOK
step s a = (ou, s')
phase s CID = revPH

goal (1 subgoal):
 1. a = Uact (uReview cid uid' p PID N rc)
[PROOF STEP]
unfolding ou
[PROOF STATE]
proof (prove)
using this:
a = Uact (uReview cid uid' p PID N rc) \<or> a = UUact (uuReview cid uid' p PID N rc)
outOK = outOK
step s a = (outOK, s')
phase s CID = revPH

goal (1 subgoal):
 1. a = Uact (uReview cid uid' p PID N rc)
[PROOF STEP]
apply (auto simp: uu_defs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6. \<lbrakk>phase s CID = revPH; a = UUact (uuReview cid uid' (pass s uid') PID N rc); cid \<in>\<in> confIDs s; uid' \<in>\<in> userIDs s; PID \<in>\<in> paperIDs s cid; phase s cid = disPH; isRev s cid uid' PID; getReviewIndex s cid uid' PID = N; paper s PID = Paper x1 x2 x3 x4 x5 x6; p = pass s uid'; s' = s\<lparr>paper := (paper s)(PID := Paper x1 x2 x3 (x4[N := rc # x4 ! N]) x5 x6)\<rparr>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using PID paperIDs_equals rs
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> paperIDs s CID
\<lbrakk>reach ?s; ?papID \<in>\<in> paperIDs ?s ?confID1.0; ?papID \<in>\<in> paperIDs ?s ?confID2.0\<rbrakk> \<Longrightarrow> ?confID1.0 = ?confID2.0
reach s

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6. \<lbrakk>phase s CID = revPH; a = UUact (uuReview cid uid' (pass s uid') PID N rc); cid \<in>\<in> confIDs s; uid' \<in>\<in> userIDs s; PID \<in>\<in> paperIDs s cid; phase s cid = disPH; isRev s cid uid' PID; getReviewIndex s cid uid' PID = N; paper s PID = Paper x1 x2 x3 x4 x5 x6; p = pass s uid'; s' = s\<lparr>paper := (paper s)(PID := Paper x1 x2 x3 (x4[N := rc # x4 ! N]) x5 x6)\<rparr>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
a = Uact (uReview cid uid' p PID N rc)

goal (1 subgoal):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
have cid: "cid = CID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cid = CID
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')

goal (1 subgoal):
 1. cid = CID
[PROOF STEP]
unfolding a
[PROOF STATE]
proof (prove)
using this:
step s (Uact (uReview cid uid' p PID N rc)) = (ou, s')

goal (1 subgoal):
 1. cid = CID
[PROOF STEP]
apply(simp add: u_defs uu_defs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 x5 x6. \<lbrakk>cid \<in>\<in> confIDs s; uid' \<in>\<in> userIDs s; PID \<in>\<in> paperIDs s cid; pass s uid' = p; phase s cid = revPH; isRev s cid uid' PID; getReviewIndex s cid uid' PID = N; paper s PID = Paper x1 x2 x3 x4 x5 x6; outOK = ou \<and> s\<lparr>paper := (paper s)(PID := Paper x1 x2 x3 (x4[N := rc # emptyReview]) x5 x6)\<rparr> = s'\<rbrakk> \<Longrightarrow> cid = CID
 2. \<lbrakk>isRev s' cid uid' PID \<longrightarrow> phase s' cid = revPH \<longrightarrow> pass s' uid' = p \<longrightarrow> PID \<in>\<in> paperIDs s' cid \<longrightarrow> uid' \<in>\<in> userIDs s' \<longrightarrow> cid \<in>\<in> confIDs s' \<longrightarrow> getReviewIndex s' cid uid' PID \<noteq> N; outErr = ou \<and> s = s'\<rbrakk> \<Longrightarrow> cid = CID
[PROOF STEP]
apply (metis PID e_updateReview_def isRev_paperIDs paperIDs_equals rs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isRev s' cid uid' PID \<longrightarrow> phase s' cid = revPH \<longrightarrow> pass s' uid' = p \<longrightarrow> PID \<in>\<in> paperIDs s' cid \<longrightarrow> uid' \<in>\<in> userIDs s' \<longrightarrow> cid \<in>\<in> confIDs s' \<longrightarrow> getReviewIndex s' cid uid' PID \<noteq> N; outErr = ou \<and> s = s'\<rbrakk> \<Longrightarrow> cid = CID
[PROOF STEP]
by (metis ou out.distinct(1))
[PROOF STATE]
proof (state)
this:
cid = CID

goal (1 subgoal):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
hence \<gamma>: "\<not> \<gamma> ?trn"
[PROOF STATE]
proof (prove)
using this:
cid = CID

goal (1 subgoal):
 1. \<not> \<gamma> (Trans s a ou s')
[PROOF STEP]
using step T rsT
[PROOF STATE]
proof (prove)
using this:
cid = CID
step s a = (ou, s')
\<not> T (Trans s a ou s')
reachNT s

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

goal (1 subgoal):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
hence f: "f ?trn = (revPH,u)"
[PROOF STATE]
proof (prove)
using this:
\<not> \<gamma> (Trans s a ou s')

goal (1 subgoal):
 1. f (Trans s a ou s') = (revPH, u)
[PROOF STEP]
using c \<phi> ph
[PROOF STATE]
proof (prove)
using this:
\<not> \<gamma> (Trans s a ou s')
consume (Trans s a ou s') vl vll'
\<phi> (Trans s a ou s')
phase s CID = revPH

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

goal (1 subgoal):
 1. f (Trans s a ou s') = (revPH, u)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (Trans s a ou s') = (revPH, u)

goal (1 subgoal):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
have u: "u = rc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u = rc
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
f (Trans s a ou s') = (revPH, u)

goal (1 subgoal):
 1. u = rc
[PROOF STEP]
unfolding a
[PROOF STATE]
proof (prove)
using this:
f (Trans s (Uact (uReview cid uid' p PID N rc)) ou s') = (revPH, u)

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

goal (1 subgoal):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
have s's: "eqExcPID_N s' s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID_N s' s
[PROOF STEP]
using eqExcPID_N_sym[OF \<phi>_step_eqExcPID_N[OF \<phi> step]]
[PROOF STATE]
proof (prove)
using this:
eqExcPID_N s' s

goal (1 subgoal):
 1. eqExcPID_N s' s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
eqExcPID_N s' s

goal (1 subgoal):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
have s's1: "eqExcPID_N s' s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID_N s' s1
[PROOF STEP]
using eqExcPID_N_trans[OF s's ss1]
[PROOF STATE]
proof (prove)
using this:
eqExcPID_N s' s1

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

goal (1 subgoal):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
have ph': "phase s' CID = revPH"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phase s' CID = revPH
[PROOF STEP]
using s's ph
[PROOF STATE]
proof (prove)
using this:
eqExcPID_N s' s
phase s CID = revPH

goal (1 subgoal):
 1. phase s' CID = revPH
[PROOF STEP]
unfolding eqExcPID_N_def
[PROOF STATE]
proof (prove)
using this:
confIDs s' = confIDs s \<and> conf s' = conf s \<and> userIDs s' = userIDs s \<and> pass s' = pass s \<and> user s' = user s \<and> roles s' = roles s \<and> paperIDs s' = paperIDs s \<and> eeqExcPID_N (paper s') (paper s) \<and> pref s' = pref s \<and> voronkov s' = voronkov s \<and> news s' = news s \<and> phase s' = phase s
phase s CID = revPH

goal (1 subgoal):
 1. phase s' CID = revPH
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
phase s' CID = revPH

goal (1 subgoal):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
proof(cases "ul' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
 2. ul' \<noteq> emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
ul' \<noteq> emptyReview

goal (2 subgoals):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
 2. ul' \<noteq> emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
note ul' = False
[PROOF STATE]
proof (state)
this:
ul' \<noteq> emptyReview

goal (2 subgoals):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
 2. ul' \<noteq> emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
hence ul'ul1: "last ul' = last ul1"
[PROOF STATE]
proof (prove)
using this:
ul' \<noteq> emptyReview

goal (1 subgoal):
 1. last ul' = last ul1
[PROOF STEP]
using ulul1
[PROOF STATE]
proof (prove)
using this:
ul' \<noteq> emptyReview
ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1

goal (1 subgoal):
 1. last ul' = last ul1
[PROOF STEP]
unfolding ul
[PROOF STATE]
proof (prove)
using this:
ul' \<noteq> emptyReview
u # ul' \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last (u # ul') = last ul1

goal (1 subgoal):
 1. last ul' = last ul1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
last ul' = last ul1

goal (2 subgoals):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
 2. ul' \<noteq> emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
have ?ignore
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> \<gamma> (Trans s a ou s')
 2. \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
[PROOF STEP]
show "\<not> \<gamma> ?trn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<gamma> (Trans s a ou s')
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<not> \<gamma> (Trans s a ou s')

goal (1 subgoal):
 1. \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
[PROOF STEP]
show "?\<Delta> s' vll' s1 vl1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
[PROOF STEP]
proof(cases "?ph' = revPH")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. phase s' CID = revPH \<Longrightarrow> \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
 2. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
phase s' CID = revPH

goal (2 subgoals):
 1. phase s' CID = revPH \<Longrightarrow> \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
 2. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
[PROOF STEP]
hence "\<Delta>3 s' vll' s1 vl1"
[PROOF STATE]
proof (prove)
using this:
phase s' CID = revPH

goal (1 subgoal):
 1. \<Delta>3 s' vll' s1 vl1
[PROOF STEP]
unfolding \<Delta>3_def B_def
[PROOF STATE]
proof (prove)
using this:
phase s' CID = revPH

goal (1 subgoal):
 1. \<exists>cid uid. PID \<in>\<in> paperIDs s' cid \<and> phase s' cid = revPH \<and> isREVNth s' uid PID N \<and> eqExcPID_N s' s1 \<and> (\<exists>ul ul1 wl. vll' = map (Pair revPH) ul @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1)
[PROOF STEP]
using ph PID s's1 PID'
[PROOF STATE]
proof (prove)
using this:
phase s' CID = revPH
phase s CID = revPH
PID \<in>\<in> paperIDs s CID
eqExcPID_N s' s1
PID \<in>\<in> paperIDs s' CID

goal (1 subgoal):
 1. \<exists>cid uid. PID \<in>\<in> paperIDs s' cid \<and> phase s' cid = revPH \<and> isREVNth s' uid PID N \<and> eqExcPID_N s' s1 \<and> (\<exists>ul ul1 wl. vll' = map (Pair revPH) ul @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>phase s' CID = revPH; phase s CID = revPH; PID \<in>\<in> paperIDs s CID; eqExcPID_N s' s1; PID \<in>\<in> paperIDs s' CID\<rbrakk> \<Longrightarrow> \<exists>cid uid. PID \<in>\<in> paperIDs s' cid \<and> phase s' cid = revPH \<and> isREVNth s' uid PID N \<and> eqExcPID_N s' s1 \<and> (\<exists>ul ul1 wl. vll' = map (Pair revPH) ul @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1)
[PROOF STEP]
apply(rule exI[of _ CID])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>phase s' CID = revPH; phase s CID = revPH; PID \<in>\<in> paperIDs s CID; eqExcPID_N s' s1; PID \<in>\<in> paperIDs s' CID\<rbrakk> \<Longrightarrow> \<exists>uid. PID \<in>\<in> paperIDs s' CID \<and> phase s' CID = revPH \<and> isREVNth s' uid PID N \<and> eqExcPID_N s' s1 \<and> (\<exists>ul ul1 wl. vll' = map (Pair revPH) ul @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1)
[PROOF STEP]
apply(rule exI[of _ uid])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>phase s' CID = revPH; phase s CID = revPH; PID \<in>\<in> paperIDs s CID; eqExcPID_N s' s1; PID \<in>\<in> paperIDs s' CID\<rbrakk> \<Longrightarrow> PID \<in>\<in> paperIDs s' CID \<and> phase s' CID = revPH \<and> isREVNth s' uid PID N \<and> eqExcPID_N s' s1 \<and> (\<exists>ul ul1 wl. vll' = map (Pair revPH) ul @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>phase s' CID = revPH; phase s CID = revPH; PID \<in>\<in> paperIDs s CID; eqExcPID_N s' s1; PID \<in>\<in> paperIDs s' CID\<rbrakk> \<Longrightarrow> isREVNth s' uid PID N
 2. \<lbrakk>phase s' CID = revPH; phase s CID = revPH; PID \<in>\<in> paperIDs s CID; eqExcPID_N s' s1; PID \<in>\<in> paperIDs s' CID\<rbrakk> \<Longrightarrow> \<exists>ul ul1 wl. vll' = map (Pair revPH) ul @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>phase s' CID = revPH; phase s CID = revPH; PID \<in>\<in> paperIDs s CID; eqExcPID_N s' s1; PID \<in>\<in> paperIDs s' CID\<rbrakk> \<Longrightarrow> isREVNth s' uid PID N
[PROOF STEP]
using uuid'
[PROOF STATE]
proof (prove)
using this:
isREVNth s' uid PID N

goal (1 subgoal):
 1. \<lbrakk>phase s' CID = revPH; phase s CID = revPH; PID \<in>\<in> paperIDs s CID; eqExcPID_N s' s1; PID \<in>\<in> paperIDs s' CID\<rbrakk> \<Longrightarrow> isREVNth s' uid PID N
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>phase s' CID = revPH; phase s CID = revPH; PID \<in>\<in> paperIDs s CID; eqExcPID_N s' s1; PID \<in>\<in> paperIDs s' CID\<rbrakk> \<Longrightarrow> \<exists>ul ul1 wl. vll' = map (Pair revPH) ul @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>phase s' CID = revPH; phase s CID = revPH; PID \<in>\<in> paperIDs s CID; eqExcPID_N s' s1; PID \<in>\<in> paperIDs s' CID\<rbrakk> \<Longrightarrow> \<exists>ul ul1 wl. vll' = map (Pair revPH) ul @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1
[PROOF STEP]
apply(rule exI[of _ ul'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>phase s' CID = revPH; phase s CID = revPH; PID \<in>\<in> paperIDs s CID; eqExcPID_N s' s1; PID \<in>\<in> paperIDs s' CID\<rbrakk> \<Longrightarrow> \<exists>ul1 wl. vll' = map (Pair revPH) ul' @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul' \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul' = last ul1
[PROOF STEP]
apply(rule exI[of _ ul1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>phase s' CID = revPH; phase s CID = revPH; PID \<in>\<in> paperIDs s CID; eqExcPID_N s' s1; PID \<in>\<in> paperIDs s' CID\<rbrakk> \<Longrightarrow> \<exists>wl. vll' = map (Pair revPH) ul' @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul' \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul' = last ul1
[PROOF STEP]
apply(rule exI[of _ wl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>phase s' CID = revPH; phase s CID = revPH; PID \<in>\<in> paperIDs s CID; eqExcPID_N s' s1; PID \<in>\<in> paperIDs s' CID\<rbrakk> \<Longrightarrow> vll' = map (Pair revPH) ul' @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul' \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul' = last ul1
[PROOF STEP]
unfolding vll'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>phase s' CID = revPH; phase s CID = revPH; PID \<in>\<in> paperIDs s CID; eqExcPID_N s' s1; PID \<in>\<in> paperIDs s' CID\<rbrakk> \<Longrightarrow> vl' = map (Pair revPH) ul' @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul' \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul' = last ul1
[PROOF STEP]
using vl'_wl vl1_wl ul'ul1 ul' ulul1
[PROOF STATE]
proof (prove)
using this:
vl' = map (Pair revPH) ul' @ map (Pair disPH) wl
vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl
last ul' = last ul1
ul' \<noteq> emptyReview
ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1

goal (1 subgoal):
 1. \<lbrakk>phase s' CID = revPH; phase s CID = revPH; PID \<in>\<in> paperIDs s CID; eqExcPID_N s' s1; PID \<in>\<in> paperIDs s' CID\<rbrakk> \<Longrightarrow> vl' = map (Pair revPH) ul' @ map (Pair disPH) wl \<and> vl1 = map (Pair revPH) ul1 @ map (Pair disPH) wl \<and> ul' \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul' = last ul1
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<Delta>3 s' vll' s1 vl1

goal (2 subgoals):
 1. phase s' CID = revPH \<Longrightarrow> \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
 2. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Delta>3 s' vll' s1 vl1

goal (1 subgoal):
 1. \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1

goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
phase s' CID \<noteq> revPH

goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
[PROOF STEP]
hence "?ph' > revPH"
[PROOF STATE]
proof (prove)
using this:
phase s' CID \<noteq> revPH

goal (1 subgoal):
 1. revPH < phase s' CID
[PROOF STEP]
using rs step ph'
[PROOF STATE]
proof (prove)
using this:
phase s' CID \<noteq> revPH
reach s
step s a = (ou, s')
phase s' CID = revPH

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

goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
[PROOF STEP]
hence "\<Delta>e s' vll' s1 vl1"
[PROOF STATE]
proof (prove)
using this:
revPH < phase s' CID

goal (1 subgoal):
 1. \<Delta>e s' vll' s1 vl1
[PROOF STEP]
unfolding \<Delta>e_def vll' vl'_wl
[PROOF STATE]
proof (prove)
using this:
revPH < phase s' CID

goal (1 subgoal):
 1. map (Pair revPH) ul' @ map (Pair disPH) wl \<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 (map (Pair revPH) ul' @ map (Pair disPH) wl)) = revPH))
[PROOF STEP]
using ul' PID'
[PROOF STATE]
proof (prove)
using this:
revPH < phase s' CID
ul' \<noteq> emptyReview
PID \<in>\<in> paperIDs s' CID

goal (1 subgoal):
 1. map (Pair revPH) ul' @ map (Pair disPH) wl \<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 (map (Pair revPH) ul' @ map (Pair disPH) wl)) = revPH))
[PROOF STEP]
by (cases ul') auto
[PROOF STATE]
proof (state)
this:
\<Delta>e s' vll' s1 vl1

goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Delta>e s' vll' s1 vl1

goal (1 subgoal):
 1. \<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Delta>3 s' vll' s1 vl1 \<or> \<Delta>4 s' vll' s1 vl1 \<or> \<Delta>e s' vll' s1 vl1

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

goal (2 subgoals):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
 2. ul' \<noteq> emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'

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

goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ul' = emptyReview

goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
note ul' = True
[PROOF STATE]
proof (state)
this:
ul' = emptyReview

goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
hence ul: "ul = [u]"
[PROOF STATE]
proof (prove)
using this:
ul' = emptyReview

goal (1 subgoal):
 1. ul = u # emptyReview
[PROOF STEP]
unfolding ul
[PROOF STATE]
proof (prove)
using this:
ul' = emptyReview

goal (1 subgoal):
 1. u # ul' = u # emptyReview
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ul = u # emptyReview

goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
(* the transition to \<Delta>4: \<phi> holds and both ul and ul1 (the parts of vl and vl1 that
cover the reviewing phase) are singletons: *)
[PROOF STATE]
proof (state)
this:
ul = u # emptyReview

goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
hence u1u: "u1 = u"
[PROOF STATE]
proof (prove)
using this:
ul = u # emptyReview

goal (1 subgoal):
 1. u1 = u
[PROOF STEP]
using ulul1
[PROOF STATE]
proof (prove)
using this:
ul = u # emptyReview
ul \<noteq> emptyReview \<and> ul1 \<noteq> emptyReview \<and> last ul = last ul1

goal (1 subgoal):
 1. u1 = u
[PROOF STEP]
unfolding ul1
[PROOF STATE]
proof (prove)
using this:
ul = u # emptyReview
ul \<noteq> emptyReview \<and> u1 # emptyReview \<noteq> emptyReview \<and> last ul = last (u1 # emptyReview)

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

goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
obtain s1' ou1 where step1: "step s1 a = (ou1,s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ou1 s1'. step s1 a = (ou1, s1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod.exhaust)
[PROOF STATE]
proof (state)
this:
step s1 a = (ou1, s1')

goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
let ?trn1 = "Trans s1 a ou1 s1'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
have \<phi>1: "\<phi> ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
using eqExcPID_N_step_\<phi>_imp[OF ss1 step step1 \<phi>]
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 a ou1 s1')

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

goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
hence ou1: "ou1 = outOK"
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 a ou1 s1')

goal (1 subgoal):
 1. ou1 = outOK
[PROOF STEP]
unfolding \<phi>_def2
[PROOF STATE]
proof (prove)
using this:
ou1 = outOK \<and> (\<exists>cid uid p rc. a = Uact (uReview cid uid p PID N rc) \<or> a = UUact (uuReview cid uid p PID N rc))

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

goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
have "PID \<in>\<in> paperIDs s1 CID" "\<exists> uid. isRevNth s1 CID uid PID N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PID \<in>\<in> paperIDs s1 CID &&& \<exists>uid. isRevNth s1 CID uid PID N
[PROOF STEP]
using eqExcPID_N_imp[OF ss1] PID uid
[PROOF STATE]
proof (prove)
using this:
confIDs s = confIDs s1 \<and> conf s = conf s1 \<and> userIDs s = userIDs s1 \<and> pass s = pass s1 \<and> user s = user s1 \<and> roles s = roles s1 \<and> paperIDs s = paperIDs s1 \<and> eeqExcPID_N (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1 \<and> getAllPaperIDs s = getAllPaperIDs s1 \<and> isRev s ?cid ?uid ?pid = isRev s1 ?cid ?uid ?pid \<and> getReviewIndex s ?cid ?uid ?pid = getReviewIndex s1 ?cid ?uid ?pid \<and> getRevRole s ?cid ?uid ?pid = getRevRole s1 ?cid ?uid ?pid \<and> length (reviewsPaper (paper s ?pid)) = length (reviewsPaper (paper s1 ?pid))
PID \<in>\<in> paperIDs s CID
isRevNth s CID uid PID N

goal (1 subgoal):
 1. PID \<in>\<in> paperIDs s1 CID &&& \<exists>uid. isRevNth s1 CID uid PID N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
PID \<in>\<in> paperIDs s1 CID
\<exists>uid. isRevNth s1 CID uid PID N

goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
hence many_s1': "revPH \<le> phase s1' CID" "PID \<in>\<in> paperIDs s1' CID"
          "\<exists>uid. isRevNth s1' CID uid PID N"
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> paperIDs s1 CID
\<exists>uid. isRevNth s1 CID uid PID N

goal (1 subgoal):
 1. revPH \<le> phase s1' CID &&& PID \<in>\<in> paperIDs s1' CID &&& \<exists>uid. isRevNth s1' CID uid PID N
[PROOF STEP]
by (metis ph1 phase_increases step1 paperIDs_mono a
                    eqExcPID_N_step_eq ou rs ss1 step step1 uid')+
[PROOF STATE]
proof (state)
this:
revPH \<le> phase s1' CID
PID \<in>\<in> paperIDs s1' CID
\<exists>uid. isRevNth s1' CID uid PID N

goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
hence uuid1': "\<exists>uid. isREVNth s1' uid PID N"
[PROOF STATE]
proof (prove)
using this:
revPH \<le> phase s1' CID
PID \<in>\<in> paperIDs s1' CID
\<exists>uid. isRevNth s1' CID uid PID N

goal (1 subgoal):
 1. \<exists>uid. isREVNth s1' uid PID N
[PROOF STEP]
by (metis isREVNth_def)
[PROOF STATE]
proof (state)
this:
\<exists>uid. isREVNth s1' uid PID N

goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
have ?match
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[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>3 s' vll' ?s1' ?vl1' \<or> \<Delta>4 s' vll' ?s1' ?vl1' \<or> \<Delta>e s' vll' ?s1' ?vl1'
[PROOF STEP]
show "validTrans ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validTrans (Trans s1 a ou1 s1')
[PROOF STEP]
using step1
[PROOF STATE]
proof (prove)
using this:
step s1 a = (ou1, s1')

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

goal (4 subgoals):
 1. consume (Trans s1 a ou1 s1') vl1 ?vl1'
 2. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
 3. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 4. \<Delta>3 s' vll' s1' ?vl1' \<or> \<Delta>4 s' vll' s1' ?vl1' \<or> \<Delta>e s' vll' s1' ?vl1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. consume (Trans s1 a ou1 s1') vl1 ?vl1'
 2. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
 3. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 4. \<Delta>3 s' vll' s1' ?vl1' \<or> \<Delta>4 s' vll' s1' ?vl1' \<or> \<Delta>e s' vll' s1' ?vl1'
[PROOF STEP]
show "consume ?trn1 vl1 (map (Pair disPH) wl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consume (Trans s1 a ou1 s1') vl1 (map (Pair disPH) wl)
[PROOF STEP]
using \<phi>1 ph1
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 a ou1 s1')
phase s1 CID = revPH

goal (1 subgoal):
 1. consume (Trans s1 a ou1 s1') vl1 (map (Pair disPH) wl)
[PROOF STEP]
unfolding consume_def
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 a ou1 s1')
phase s1 CID = revPH

goal (1 subgoal):
 1. if \<phi> (Trans s1 a ou1 s1') then vl1 \<noteq> [] \<and> f (Trans s1 a ou1 s1') = hd vl1 \<and> map (Pair disPH) wl = tl vl1 else map (Pair disPH) wl = vl1
[PROOF STEP]
by (simp add: a ul1 vl1_wl ul1 u1u u ph1 cid)
[PROOF STATE]
proof (state)
this:
consume (Trans s1 a ou1 s1') vl1 (map (Pair disPH) wl)

goal (3 subgoals):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
 2. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 3. \<Delta>3 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>4 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>e s' vll' s1' (map (Pair disPH) wl)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
 2. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 3. \<Delta>3 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>4 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>e s' vll' s1' (map (Pair disPH) wl)
[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 ou1 s1')
[PROOF STEP]
unfolding ss1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')

goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 2. \<Delta>3 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>4 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>e s' vll' s1' (map (Pair disPH) wl)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 2. \<Delta>3 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>4 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>e s' vll' s1' (map (Pair disPH) wl)
[PROOF STEP]
assume "\<gamma> ?trn"
[PROOF STATE]
proof (state)
this:
\<gamma> (Trans s a ou s')

goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 2. \<Delta>3 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>4 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>e s' vll' s1' (map (Pair disPH) wl)
[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 ou1 s1')
[PROOF STEP]
using eqExcPID_N_step_out[OF ss1 step step1 rsT rs1 PID ph]
[PROOF STATE]
proof (prove)
using this:
\<gamma> (Trans s a ou s')
userOfA a \<in> UIDs \<Longrightarrow> ou = ou1

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

goal (1 subgoal):
 1. \<Delta>3 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>4 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>e s' vll' s1' (map (Pair disPH) wl)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>3 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>4 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>e s' vll' s1' (map (Pair disPH) wl)
[PROOF STEP]
note s's1' = eqExcPID_N_step_eq[OF rs ss1 a step[unfolded ou] step1]
[PROOF STATE]
proof (state)
this:
s' = s1'

goal (1 subgoal):
 1. \<Delta>3 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>4 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>e s' vll' s1' (map (Pair disPH) wl)
[PROOF STEP]
have "\<Delta>4 s' vll' s1' (map (Pair disPH) wl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>4 s' vll' s1' (map (Pair disPH) wl)
[PROOF STEP]
unfolding \<Delta>4_def B_def
[PROOF STATE]
proof (prove)
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' = s1' \<and> (\<exists>wla. vll' = map (Pair disPH) wla \<and> map (Pair disPH) wl = map (Pair disPH) wla)
[PROOF STEP]
using ph PID s's1' many_s1' uuid1'
[PROOF STATE]
proof (prove)
using this:
phase s CID = revPH
PID \<in>\<in> paperIDs s CID
s' = s1'
revPH \<le> phase s1' CID
PID \<in>\<in> paperIDs s1' CID
\<exists>uid. isRevNth s1' CID uid PID N
\<exists>uid. isREVNth s1' 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' = s1' \<and> (\<exists>wla. vll' = map (Pair disPH) wla \<and> map (Pair disPH) wl = map (Pair disPH) wla)
[PROOF STEP]
unfolding vll' vl'_wl ul'
[PROOF STATE]
proof (prove)
using this:
phase s CID = revPH
PID \<in>\<in> paperIDs s CID
s' = s1'
revPH \<le> phase s1' CID
PID \<in>\<in> paperIDs s1' CID
\<exists>uid. isRevNth s1' CID uid PID N
\<exists>uid. isREVNth s1' 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' = s1' \<and> (\<exists>wla. map (Pair revPH) emptyReview @ 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' vll' s1' (map (Pair disPH) wl)

goal (1 subgoal):
 1. \<Delta>3 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>4 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>e s' vll' s1' (map (Pair disPH) wl)
[PROOF STEP]
thus "?\<Delta> s' vll' s1' (map (Pair disPH) wl)"
[PROOF STATE]
proof (prove)
using this:
\<Delta>4 s' vll' s1' (map (Pair disPH) wl)

goal (1 subgoal):
 1. \<Delta>3 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>4 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>e s' vll' s1' (map (Pair disPH) wl)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Delta>3 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>4 s' vll' s1' (map (Pair disPH) wl) \<or> \<Delta>e s' vll' s1' (map (Pair disPH) wl)

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

goal (1 subgoal):
 1. ul' = emptyReview \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
match (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vll'

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

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

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

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

goal (1 subgoal):
 1. ul1' = emptyReview \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<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>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
using vl
[PROOF STATE]
proof (prove)
using this:
reaction (\<lambda>s vl s1 vl1. \<Delta>3 s vl s1 vl1 \<or> \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
vl = (revPH, u) # vl'

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

goal:
No subgoals!
[PROOF STEP]
qed