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

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

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

goal (1 subgoal):
 1. (\<And>CID. \<lbrakk>\<nexists>uid. isREVNth s uid PID N; PID \<in>\<in> paperIDs s CID; reach s; phase s CID = revPH; s1 = s; B vl vl1; vl \<noteq> []; vl1 \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<Delta>2_def B_def
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
\<exists>cid. PID \<in>\<in> paperIDs s cid \<and> phase s cid = revPH \<and> (\<nexists>uid. isREVNth s uid PID N) \<and> 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>CID. \<lbrakk>\<nexists>uid. isREVNth s uid PID N; PID \<in>\<in> paperIDs s CID; reach s; phase s CID = revPH; s1 = s; \<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> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>uid. isREVNth s uid PID N
PID \<in>\<in> paperIDs s CID
reach s
phase s CID = revPH
s1 = s
B vl vl1
vl \<noteq> []
vl1 \<noteq> []

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>2 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
hence uid: "\<not> (\<exists> uid. isRevNth s CID uid PID N)"
[PROOF STATE]
proof (prove)
using this:
\<nexists>uid. isREVNth s uid PID N
PID \<in>\<in> paperIDs s CID
reach s
phase s CID = revPH
s1 = s
B vl vl1
vl \<noteq> []
vl1 \<noteq> []

goal (1 subgoal):
 1. \<nexists>uid. isRevNth s CID uid PID N
[PROOF STEP]
by (metis isREVNth_def)
[PROOF STATE]
proof (state)
this:
\<nexists>uid. isRevNth s CID uid PID N

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>2 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iaction (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
fix a :: act and ou :: out and s' :: state and vl'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ou s' vl'. \<lbrakk>step s a = (ou, s'); \<not> T (Trans s a ou s'); consume (Trans s a ou s') vl vl'\<rbrakk> \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
let ?trn1 = "Trans s1 a ou s'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ou s' vl'. \<lbrakk>step s a = (ou, s'); \<not> T (Trans s a ou s'); consume (Trans s a ou s') vl vl'\<rbrakk> \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
assume step: "step s a = (ou, s')" and T: "\<not> T ?trn" and c: "consume ?trn vl vl'"
[PROOF STATE]
proof (state)
this:
step s a = (ou, s')
\<not> T (Trans s a ou s')
consume (Trans s a ou s') vl vl'

goal (1 subgoal):
 1. \<And>a ou s' vl'. \<lbrakk>step s a = (ou, s'); \<not> T (Trans s a ou s'); consume (Trans s a ou s') vl vl'\<rbrakk> \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
have \<phi>: "\<not> \<phi> ?trn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. a = Cact x1 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 2. \<And>x2. a = Uact x2 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 3. \<And>x3. a = UUact x3 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 4. \<And>x4. a = Ract x4 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 5. \<And>x5. a = Lact x5 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = Cact x1_ \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. a = Uact x2 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 2. \<And>x3. a = UUact x3 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 3. \<And>x4. a = Ract x4 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 4. \<And>x5. a = Lact x5 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = Uact x2 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
apply(cases x2)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>a = Uact x2; x2 = uUser x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 2. \<And>x21 x22 x23. \<lbrakk>a = Uact x2; x2 = uConfA x21 x22 x23\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 3. \<And>x31 x32 x33 x34. \<lbrakk>a = Uact x2; x2 = uPhase x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 4. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 5. \<And>x51 x52 x53 x54 x55. \<lbrakk>a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 6. \<And>x61 x62 x63 x64 x65. \<lbrakk>a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 7. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
using step ph
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
phase s CID = revPH

goal (7 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>a = Uact x2; x2 = uUser x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 2. \<And>x21 x22 x23. \<lbrakk>a = Uact x2; x2 = uConfA x21 x22 x23\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 3. \<And>x31 x32 x33 x34. \<lbrakk>a = Uact x2; x2 = uPhase x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 4. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 5. \<And>x51 x52 x53 x54 x55. \<lbrakk>a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 6. \<And>x61 x62 x63 x64 x65. \<lbrakk>a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 7. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
apply (auto simp: u_defs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x71 x72 aa aaa b x1 x2a x3 x4 x5 x6. \<lbrakk>phase s CID = revPH; a = Uact (uReview x71 x72 (pass s x72) PID N (aa, aaa, b)); x2 = uReview x71 x72 (pass s x72) PID N (aa, aaa, b); x71 \<in>\<in> confIDs s; x72 \<in>\<in> userIDs s; PID \<in>\<in> paperIDs s x71; phase s x71 = revPH; isRev s x71 x72 PID; paper s PID = Paper x1 x2a x3 x4 x5 x6; ou = outOK; s' = s\<lparr>paper := (paper s)(PID := Paper x1 x2a x3 (x4[N := (aa, aaa, b) # emptyReview]) x5 x6)\<rparr>; getReviewIndex s x71 x72 PID = N\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis PID isRev_imp_isRevNth_getReviewIndex paperIDs_equals rs uid)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. a = UUact x3 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 2. \<And>x4. a = Ract x4 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 3. \<And>x5. a = Lact x5 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = UUact x3 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
apply(cases x3)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>a = UUact x3; x3 = uuNews x11 x12 x13 x14\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>a = UUact x3; x3 = uuDis x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 3. \<And>x31 x32 x33 x34 x35 x36. \<lbrakk>a = UUact x3; x3 = uuReview x31 x32 x33 x34 x35 x36\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>a = UUact x3; x3 = uuDec x41 x42 x43 x44 x45\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
using step ph
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
phase s CID = revPH

goal (4 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>a = UUact x3; x3 = uuNews x11 x12 x13 x14\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>a = UUact x3; x3 = uuDis x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 3. \<And>x31 x32 x33 x34 x35 x36. \<lbrakk>a = UUact x3; x3 = uuReview x31 x32 x33 x34 x35 x36\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>a = UUact x3; x3 = uuDec x41 x42 x43 x44 x45\<rbrakk> \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
apply (auto simp: uu_defs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 aa aaa b x1 x2 x3a x4 x5 x6. \<lbrakk>phase s CID = revPH; a = UUact (uuReview x31 x32 (pass s x32) PID N (aa, aaa, b)); x3 = uuReview x31 x32 (pass s x32) PID N (aa, aaa, b); x31 \<in>\<in> confIDs s; x32 \<in>\<in> userIDs s; PID \<in>\<in> paperIDs s x31; phase s x31 = disPH; isRev s x31 x32 PID; paper s PID = Paper x1 x2 x3a x4 x5 x6; ou = outOK; s' = s\<lparr>paper := (paper s)(PID := Paper x1 x2 x3a (x4[N := (aa, aaa, b) # x4 ! N]) x5 x6)\<rparr>; getReviewIndex s x31 x32 PID = N\<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>x31 x32 aa aaa b x1 x2 x3a x4 x5 x6. \<lbrakk>phase s CID = revPH; a = UUact (uuReview x31 x32 (pass s x32) PID N (aa, aaa, b)); x3 = uuReview x31 x32 (pass s x32) PID N (aa, aaa, b); x31 \<in>\<in> confIDs s; x32 \<in>\<in> userIDs s; PID \<in>\<in> paperIDs s x31; phase s x31 = disPH; isRev s x31 x32 PID; paper s PID = Paper x1 x2 x3a x4 x5 x6; ou = outOK; s' = s\<lparr>paper := (paper s)(PID := Paper x1 x2 x3a (x4[N := (aa, aaa, b) # x4 ! N]) x5 x6)\<rparr>; getReviewIndex s x31 x32 PID = N\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. a = Ract x4 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
 2. \<And>x5. a = Lact x5 \<Longrightarrow> \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<not> \<phi> (Trans s a ou s')

goal (1 subgoal):
 1. \<And>a ou s' vl'. \<lbrakk>step s a = (ou, s'); \<not> T (Trans s a ou s'); consume (Trans s a ou s') vl vl'\<rbrakk> \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
hence vl': "vl' = vl"
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s a ou s')

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

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

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

goal (1 subgoal):
 1. \<And>a ou s' vl'. \<lbrakk>step s a = (ou, s'); \<not> T (Trans s a ou s'); consume (Trans s a ou s') vl vl'\<rbrakk> \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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]
by (metis paperIDs_mono step PID)
[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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
show "match ?\<Delta> s s1 vl1 a ou s' vl' \<or> ignore ?\<Delta> s s1 vl1 a ou s' vl'" (is "?match \<or> ?ignore")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
have ?match
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. validTrans (Trans s1 ?a1.0 ?ou1.0 ?s1')
 2. consume (Trans s1 ?a1.0 ?ou1.0 ?s1') vl1 ?vl1'
 3. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 ?a1.0 ?ou1.0 ?s1')
 4. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 ?a1.0 ?ou1.0 ?s1')
 5. \<Delta>2 s' vl' ?s1' ?vl1' \<or> \<Delta>3 s' vl' ?s1' ?vl1' \<or> \<Delta>e s' vl' ?s1' ?vl1'
[PROOF STEP]
show "validTrans ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validTrans (Trans s1 a ou s')
[PROOF STEP]
unfolding ss1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validTrans (Trans s a ou s')
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')

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

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

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

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

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

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

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

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

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

goal (2 subgoals):
 1. phase s' CID = revPH \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
 2. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
note ph' = True
[PROOF STATE]
proof (state)
this:
phase s' CID = revPH

goal (2 subgoals):
 1. phase s' CID = revPH \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
 2. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
proof(cases "\<exists> uid. isRevNth s' CID uid PID N")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>uid. isRevNth s' CID uid PID N \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
 2. \<nexists>uid. isRevNth s' CID uid PID N \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>uid. isRevNth s' CID uid PID N

goal (2 subgoals):
 1. \<exists>uid. isRevNth s' CID uid PID N \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
 2. \<nexists>uid. isRevNth s' CID uid PID N \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
hence "\<not> (\<exists> uid. isREVNth s' uid PID N)"
[PROOF STATE]
proof (prove)
using this:
\<nexists>uid. isRevNth s' CID uid PID N

goal (1 subgoal):
 1. \<nexists>uid. isREVNth s' uid PID N
[PROOF STEP]
by (metis PID' isREVNth_def isRevNth_paperIDs paperIDs_equals reach_PairI rs1 ss1 step)
[PROOF STATE]
proof (state)
this:
\<nexists>uid. isREVNth s' uid PID N

goal (2 subgoals):
 1. \<exists>uid. isRevNth s' CID uid PID N \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
 2. \<nexists>uid. isRevNth s' CID uid PID N \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
hence "\<Delta>2 s' vl' s' vl1"
[PROOF STATE]
proof (prove)
using this:
\<nexists>uid. isREVNth s' uid PID N

goal (1 subgoal):
 1. \<Delta>2 s' vl' s' vl1
[PROOF STEP]
unfolding \<Delta>2_def vl'
[PROOF STATE]
proof (prove)
using this:
\<nexists>uid. isREVNth s' uid PID N

goal (1 subgoal):
 1. \<exists>cid. PID \<in>\<in> paperIDs s' cid \<and> phase s' cid = revPH \<and> (\<nexists>uid. isREVNth s' uid PID N) \<and> s' = s' \<and> B vl vl1
[PROOF STEP]
using B ph' PID'
[PROOF STATE]
proof (prove)
using this:
\<nexists>uid. isREVNth s' uid PID N
B vl vl1
phase s' CID = revPH
PID \<in>\<in> paperIDs s' CID

goal (1 subgoal):
 1. \<exists>cid. PID \<in>\<in> paperIDs s' cid \<and> phase s' cid = revPH \<and> (\<nexists>uid. isREVNth s' uid PID N) \<and> s' = s' \<and> B vl vl1
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>uid. isREVNth s' uid PID N
\<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
phase s' CID = revPH
PID \<in>\<in> paperIDs s' CID

goal (1 subgoal):
 1. \<exists>cid. PID \<in>\<in> paperIDs s' cid \<and> phase s' cid = revPH \<and> (\<nexists>uid. isREVNth s' uid PID N) \<and> s' = s' \<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 auto
[PROOF STATE]
proof (state)
this:
\<Delta>2 s' vl' s' vl1

goal (2 subgoals):
 1. \<exists>uid. isRevNth s' CID uid PID N \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
 2. \<nexists>uid. isRevNth s' CID uid PID N \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Delta>2 s' vl' s' vl1

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

goal (1 subgoal):
 1. \<exists>uid. isRevNth s' CID uid PID N \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>uid. isRevNth s' CID uid PID N \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>uid. isRevNth s' CID uid PID N

goal (1 subgoal):
 1. \<exists>uid. isRevNth s' CID uid PID N \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
hence "\<exists> uid. isREVNth s' uid PID N"
[PROOF STATE]
proof (prove)
using this:
\<exists>uid. isRevNth s' CID uid PID N

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

goal (1 subgoal):
 1. \<exists>uid. isRevNth s' CID uid PID N \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
hence "\<Delta>3 s' vl' s' vl1"
[PROOF STATE]
proof (prove)
using this:
\<exists>uid. isREVNth s' uid PID N

goal (1 subgoal):
 1. \<Delta>3 s' vl' s' vl1
[PROOF STEP]
unfolding \<Delta>3_def vl'
[PROOF STATE]
proof (prove)
using this:
\<exists>uid. isREVNth s' uid PID N

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' s' \<and> B vl vl1
[PROOF STEP]
using B ph' PID'
[PROOF STATE]
proof (prove)
using this:
\<exists>uid. isREVNth s' uid PID N
B vl vl1
phase s' CID = revPH
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' s' \<and> B vl vl1
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
\<exists>uid. isREVNth s' uid PID N
\<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
phase s' CID = revPH
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' s' \<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 auto
[PROOF STATE]
proof (state)
this:
\<Delta>3 s' vl' s' vl1

goal (1 subgoal):
 1. \<exists>uid. isRevNth s' CID uid PID N \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Delta>3 s' vl' s' vl1

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

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

goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' 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>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
hence ph': "?ph' > revPH"
[PROOF STATE]
proof (prove)
using this:
phase s' CID \<noteq> revPH

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

goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
hence "\<not> (\<exists> uid. isRevNth s' CID uid PID N)"
[PROOF STATE]
proof (prove)
using this:
revPH < phase s' CID

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

goal (1 subgoal):
 1. \<nexists>uid. isRevNth s' CID uid PID N
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Cact x1\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 2. \<And>x2. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Uact x2\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 3. \<And>x3. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = UUact x3\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 4. \<And>x4. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Ract x4\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 5. \<And>x5. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Lact x5\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Cact x1\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
[PROOF STEP]
apply(cases x1)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14 x15. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Cact x1; x1 = cUser x11 x12 x13 x14 x15\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Cact x1; x1 = cConf x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 3. \<And>x31 x32 x33 x34. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Cact x1; x1 = cPC x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 4. \<And>x41 x42 x43 x44. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Cact x1; x1 = cChair x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Cact x1; x1 = cPaper x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 6. \<And>x61 x62 x63 x64 x65. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Cact x1; x1 = cAuthor x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 7. \<And>x71 x72 x73 x74 x75. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Cact x1; x1 = cConflict x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 8. \<And>x81 x82 x83 x84 x85. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Cact x1; x1 = cReview x81 x82 x83 x84 x85\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
[PROOF STEP]
apply(fastforce simp: c_defs)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Uact x2\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 2. \<And>x3. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = UUact x3\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 3. \<And>x4. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Ract x4\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 4. \<And>x5. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Lact x5\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Uact x2\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
[PROOF STEP]
apply(cases x2)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Uact x2; x2 = uUser x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 2. \<And>x21 x22 x23. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Uact x2; x2 = uConfA x21 x22 x23\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 3. \<And>x31 x32 x33 x34. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Uact x2; x2 = uPhase x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 4. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 5. \<And>x51 x52 x53 x54 x55. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 6. \<And>x61 x62 x63 x64 x65. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 7. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
[PROOF STEP]
apply(fastforce simp: u_defs)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = UUact x3\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 2. \<And>x4. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Ract x4\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 3. \<And>x5. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Lact x5\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = UUact x3\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
[PROOF STEP]
apply(cases x3)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = UUact x3; x3 = uuNews x11 x12 x13 x14\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = UUact x3; x3 = uuDis x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 3. \<And>x31 x32 x33 x34 x35 x36. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = UUact x3; x3 = uuReview x31 x32 x33 x34 x35 x36\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = UUact x3; x3 = uuDec x41 x42 x43 x44 x45\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
[PROOF STEP]
apply(fastforce simp: uu_defs)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Ract x4\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
 2. \<And>x5. \<lbrakk>revPH < phase s' CID; PID \<in>\<in> paperIDs s CID; \<nexists>uid. isRevNth s CID uid PID N; phase s CID = revPH; step s a = (ou, s'); reach s; a = Lact x5\<rbrakk> \<Longrightarrow> \<nexists>uid. isRevNth s' CID uid PID N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>uid. isRevNth s' CID uid PID N

goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
hence "\<not> (\<exists> uid. isREVNth s' uid PID N)"
[PROOF STATE]
proof (prove)
using this:
\<nexists>uid. isRevNth s' CID uid PID N

goal (1 subgoal):
 1. \<nexists>uid. isREVNth s' uid PID N
[PROOF STEP]
by (metis IO_Automaton.reach_PairI PID' isREVNth_imp_isRevNth rs1 ss1 step)
[PROOF STATE]
proof (state)
this:
\<nexists>uid. isREVNth s' uid PID N

goal (1 subgoal):
 1. phase s' CID \<noteq> revPH \<Longrightarrow> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>3 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
hence "\<Delta>e s' vl' s' vl1"
[PROOF STATE]
proof (prove)
using this:
\<nexists>uid. isREVNth s' uid PID N

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

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

goal (1 subgoal):
 1. vl \<noteq> [] \<and> ((\<exists>cid. PID \<in>\<in> paperIDs s' cid \<and> revPH < phase s' cid \<and> (\<nexists>uid. isREVNth s' uid PID N)) \<or> (\<exists>cid. PID \<in>\<in> paperIDs s' cid \<and> revPH < phase s' cid \<and> fst (hd vl) = revPH))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>e s' vl' s' vl1

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

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

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

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

goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
match (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'

goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
match (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
match (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
reaction (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
vl \<noteq> []

goal (1 subgoal):
 1. iaction (\<lambda>s vl s1 vl1. \<Delta>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 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>2 s vl s1 vl1 \<or> \<Delta>3 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1

goal:
No subgoals!
[PROOF STEP]
qed