[STATEMENT]
lemma eeqExcPID_N_imp_eq:
assumes "eeqExcPID_N paps paps1"
and "reviewsPaper (paps PID) ! N = reviewsPaper (paps1 PID) ! N"
shows "paps = paps1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paps = paps1
[PROOF STEP]
proof(rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. paps x = paps1 x
[PROOF STEP]
fix pid
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. paps x = paps1 x
[PROOF STEP]
show "paps pid = paps1 pid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paps pid = paps1 pid
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eeqExcPID_N paps paps1
reviewsPaper (paps PID) ! N = reviewsPaper (paps1 PID) ! N

goal (1 subgoal):
 1. paps pid = paps1 pid
[PROOF STEP]
unfolding eeqExcPID_N_def eqExcD eqExcNth_def
[PROOF STATE]
proof (prove)
using this:
\<forall>pid. if pid = PID then titlePaper (paps pid) = titlePaper (paps1 pid) \<and> abstractPaper (paps pid) = abstractPaper (paps1 pid) \<and> contentPaper (paps pid) = contentPaper (paps1 pid) \<and> disPaper (paps pid) = disPaper (paps1 pid) \<and> decsPaper (paps pid) = decsPaper (paps1 pid) \<and> length (reviewsPaper (paps pid)) = length (reviewsPaper (paps1 pid)) \<and> (\<forall>i<length (reviewsPaper (paps pid)). i \<noteq> N \<longrightarrow> reviewsPaper (paps pid) ! i = reviewsPaper (paps1 pid) ! i) else paps pid = paps1 pid
reviewsPaper (paps PID) ! N = reviewsPaper (paps1 PID) ! N

goal (1 subgoal):
 1. paps pid = paps1 pid
[PROOF STEP]
apply(cases "paps PID", cases "paps1 PID", cases "pid = PID")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 x5 x6 x1a x2a x3a x4a x5a x6a. \<lbrakk>\<forall>pid. if pid = PID then titlePaper (paps pid) = titlePaper (paps1 pid) \<and> abstractPaper (paps pid) = abstractPaper (paps1 pid) \<and> contentPaper (paps pid) = contentPaper (paps1 pid) \<and> disPaper (paps pid) = disPaper (paps1 pid) \<and> decsPaper (paps pid) = decsPaper (paps1 pid) \<and> length (reviewsPaper (paps pid)) = length (reviewsPaper (paps1 pid)) \<and> (\<forall>i<length (reviewsPaper (paps pid)). i \<noteq> N \<longrightarrow> reviewsPaper (paps pid) ! i = reviewsPaper (paps1 pid) ! i) else paps pid = paps1 pid; reviewsPaper (paps PID) ! N = reviewsPaper (paps1 PID) ! N; paps PID = Paper x1 x2 x3 x4 x5 x6; \<forall>pid. if pid = PID then titlePaper (paps pid) = titlePaper (paps1 pid) \<and> abstractPaper (paps pid) = abstractPaper (paps1 pid) \<and> contentPaper (paps pid) = contentPaper (paps1 pid) \<and> disPaper (paps pid) = disPaper (paps1 pid) \<and> decsPaper (paps pid) = decsPaper (paps1 pid) \<and> length (reviewsPaper (paps pid)) = length (reviewsPaper (paps1 pid)) \<and> (\<forall>i<length (reviewsPaper (paps pid)). i \<noteq> N \<longrightarrow> reviewsPaper (paps pid) ! i = reviewsPaper (paps1 pid) ! i) else paps pid = paps1 pid; reviewsPaper (paps PID) ! N = reviewsPaper (paps1 PID) ! N; paps1 PID = Paper x1a x2a x3a x4a x5a x6a; \<forall>pid. if pid = PID then titlePaper (paps pid) = titlePaper (paps1 pid) \<and> abstractPaper (paps pid) = abstractPaper (paps1 pid) \<and> contentPaper (paps pid) = contentPaper (paps1 pid) \<and> disPaper (paps pid) = disPaper (paps1 pid) \<and> decsPaper (paps pid) = decsPaper (paps1 pid) \<and> length (reviewsPaper (paps pid)) = length (reviewsPaper (paps1 pid)) \<and> (\<forall>i<length (reviewsPaper (paps pid)). i \<noteq> N \<longrightarrow> reviewsPaper (paps pid) ! i = reviewsPaper (paps1 pid) ! i) else paps pid = paps1 pid; reviewsPaper (paps PID) ! N = reviewsPaper (paps1 PID) ! N; pid = PID\<rbrakk> \<Longrightarrow> paps pid = paps1 pid
 2. \<And>x1 x2 x3 x4 x5 x6 x1a x2a x3a x4a x5a x6a. \<lbrakk>\<forall>pid. if pid = PID then titlePaper (paps pid) = titlePaper (paps1 pid) \<and> abstractPaper (paps pid) = abstractPaper (paps1 pid) \<and> contentPaper (paps pid) = contentPaper (paps1 pid) \<and> disPaper (paps pid) = disPaper (paps1 pid) \<and> decsPaper (paps pid) = decsPaper (paps1 pid) \<and> length (reviewsPaper (paps pid)) = length (reviewsPaper (paps1 pid)) \<and> (\<forall>i<length (reviewsPaper (paps pid)). i \<noteq> N \<longrightarrow> reviewsPaper (paps pid) ! i = reviewsPaper (paps1 pid) ! i) else paps pid = paps1 pid; reviewsPaper (paps PID) ! N = reviewsPaper (paps1 PID) ! N; paps PID = Paper x1 x2 x3 x4 x5 x6; \<forall>pid. if pid = PID then titlePaper (paps pid) = titlePaper (paps1 pid) \<and> abstractPaper (paps pid) = abstractPaper (paps1 pid) \<and> contentPaper (paps pid) = contentPaper (paps1 pid) \<and> disPaper (paps pid) = disPaper (paps1 pid) \<and> decsPaper (paps pid) = decsPaper (paps1 pid) \<and> length (reviewsPaper (paps pid)) = length (reviewsPaper (paps1 pid)) \<and> (\<forall>i<length (reviewsPaper (paps pid)). i \<noteq> N \<longrightarrow> reviewsPaper (paps pid) ! i = reviewsPaper (paps1 pid) ! i) else paps pid = paps1 pid; reviewsPaper (paps PID) ! N = reviewsPaper (paps1 PID) ! N; paps1 PID = Paper x1a x2a x3a x4a x5a x6a; \<forall>pid. if pid = PID then titlePaper (paps pid) = titlePaper (paps1 pid) \<and> abstractPaper (paps pid) = abstractPaper (paps1 pid) \<and> contentPaper (paps pid) = contentPaper (paps1 pid) \<and> disPaper (paps pid) = disPaper (paps1 pid) \<and> decsPaper (paps pid) = decsPaper (paps1 pid) \<and> length (reviewsPaper (paps pid)) = length (reviewsPaper (paps1 pid)) \<and> (\<forall>i<length (reviewsPaper (paps pid)). i \<noteq> N \<longrightarrow> reviewsPaper (paps pid) ! i = reviewsPaper (paps1 pid) ! i) else paps pid = paps1 pid; reviewsPaper (paps PID) ! N = reviewsPaper (paps1 PID) ! N; pid \<noteq> PID\<rbrakk> \<Longrightarrow> paps pid = paps1 pid
[PROOF STEP]
by simp_all (metis nth_equalityI)
[PROOF STATE]
proof (state)
this:
paps pid = paps1 pid

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqExcPID_N_imp_eq:
assumes e: "eqExcPID_N s s1"
and "reviewsPaper (paper s PID) ! N = reviewsPaper (paper s1 PID) ! N"
shows "s = s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = s1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s = s1
[PROOF STEP]
have "paper s = paper s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paper s = paper s1
[PROOF STEP]
using assms eeqExcPID_N_imp_eq
[PROOF STATE]
proof (prove)
using this:
eqExcPID_N s s1
reviewsPaper (paper s PID) ! N = reviewsPaper (paper s1 PID) ! N
\<lbrakk>eeqExcPID_N ?paps ?paps1.0; reviewsPaper (?paps PID) ! N = reviewsPaper (?paps1.0 PID) ! N\<rbrakk> \<Longrightarrow> ?paps = ?paps1.0

goal (1 subgoal):
 1. paper s = paper s1
[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
reviewsPaper (paper s PID) ! N = reviewsPaper (paper s1 PID) ! N
\<lbrakk>eeqExcPID_N ?paps ?paps1.0; reviewsPaper (?paps PID) ! N = reviewsPaper (?paps1.0 PID) ! N\<rbrakk> \<Longrightarrow> ?paps = ?paps1.0

goal (1 subgoal):
 1. paper s = paper s1
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
paper s = paper s1

goal (1 subgoal):
 1. s = s1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
paper s = paper s1

goal (1 subgoal):
 1. s = s1
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
paper s = paper s1
eqExcPID_N s s1

goal (1 subgoal):
 1. s = s1
[PROOF STEP]
unfolding eqExcPID_N_def
[PROOF STATE]
proof (prove)
using this:
paper s = paper s1
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

goal (1 subgoal):
 1. s = s1
[PROOF STEP]
by (intro state.equality) auto
[PROOF STATE]
proof (state)
this:
s = s1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqExcPID_N_step_eq:
assumes s: "reach s" and ss1: "eqExcPID_N s s1"
and a: "a = Uact (uReview cid uid p PID N rc)"
and step: "step s a = (outOK, s')" and step1: "step s1 a = (ou', s1')"
shows "s' = s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s' = s1'
[PROOF STEP]
proof(cases "\<exists> cid uid. isRevNth s cid uid PID N")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
 2. \<nexists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>cid uid. isRevNth s cid uid PID N

goal (2 subgoals):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
 2. \<nexists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
\<nexists>cid uid. isRevNth s cid uid PID N

goal (1 subgoal):
 1. False
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<nexists>cid uid. isRevNth s cid uid PID N
step s a = (outOK, s')

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding a
[PROOF STATE]
proof (prove)
using this:
\<nexists>cid uid. isRevNth s cid uid PID N
step s (Uact (uReview cid uid p PID N rc)) = (outOK, s')

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp add: u_defs uu_defs) (metis isRev_imp_isRevNth_getReviewIndex)+
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
 2. \<nexists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>cid uid. isRevNth s cid uid PID N

goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
note r = True
[PROOF STATE]
proof (state)
this:
\<exists>cid uid. isRevNth s cid uid PID N

goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
note eqs = eqExcPID_N_imp[OF ss1]
[PROOF STATE]
proof (state)
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))

goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
note eqsT = eqExcPID_N_Paper[OF ss1]
[PROOF STATE]
proof (state)
this:
\<lbrakk>paper s ?pid = Paper ?title ?abstract ?content ?reviews ?dis ?decs; paper s1 ?pid = Paper ?title1.0 ?abstract1.0 ?content1.0 ?reviews1.0 ?dis1.0 ?decs1.0\<rbrakk> \<Longrightarrow> ?title = ?title1.0 \<and> ?abstract = ?abstract1.0 \<and> ?content = ?content1.0 \<and> ?dis = ?dis1.0 \<and> ?decs = ?decs1.0

goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
have r: "N < length (reviewsPaper (paper s PID))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N < length (reviewsPaper (paper s PID))
[PROOF STEP]
using isRevNth_less_length[OF s] r
[PROOF STATE]
proof (prove)
using this:
isRevNth s ?cid ?uid ?pid ?n \<Longrightarrow> ?n < length (reviewsPaper (paper s ?pid))
\<exists>cid uid. isRevNth s cid uid PID N

goal (1 subgoal):
 1. N < length (reviewsPaper (paper s PID))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
N < length (reviewsPaper (paper s PID))

goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
have r1: "N < length (reviewsPaper (paper s1 PID))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N < length (reviewsPaper (paper s1 PID))
[PROOF STEP]
using eqs r
[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))
N < length (reviewsPaper (paper s PID))

goal (1 subgoal):
 1. N < length (reviewsPaper (paper s1 PID))
[PROOF STEP]
unfolding eeqExcPID_N_def eqExcD eqExcNth_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> (\<forall>pid. if pid = PID then titlePaper (paper s pid) = titlePaper (paper s1 pid) \<and> abstractPaper (paper s pid) = abstractPaper (paper s1 pid) \<and> contentPaper (paper s pid) = contentPaper (paper s1 pid) \<and> disPaper (paper s pid) = disPaper (paper s1 pid) \<and> decsPaper (paper s pid) = decsPaper (paper s1 pid) \<and> length (reviewsPaper (paper s pid)) = length (reviewsPaper (paper s1 pid)) \<and> (\<forall>i<length (reviewsPaper (paper s pid)). i \<noteq> N \<longrightarrow> reviewsPaper (paper s pid) ! i = reviewsPaper (paper s1 pid) ! i) else paper s pid = paper s1 pid) \<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))
N < length (reviewsPaper (paper s PID))

goal (1 subgoal):
 1. N < length (reviewsPaper (paper s1 PID))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
N < length (reviewsPaper (paper s1 PID))

goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
have s's1': "eqExcPID_N s' s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID_N s' s1'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reach s
eqExcPID_N s s1
a = Uact (uReview cid uid p PID N rc)
step s a = (outOK, s')
step s1 a = (ou', s1')

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

goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
have "e_updateReview s cid uid p PID N rc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_updateReview s cid uid p PID N rc
[PROOF STEP]
using step a
[PROOF STATE]
proof (prove)
using this:
step s a = (outOK, s')
a = Uact (uReview cid uid p PID N rc)

goal (1 subgoal):
 1. e_updateReview s cid uid p PID N rc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e_updateReview s cid uid p PID N rc

goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
hence "e_updateReview s1 cid uid p PID N rc"
[PROOF STATE]
proof (prove)
using this:
e_updateReview s cid uid p PID N rc

goal (1 subgoal):
 1. e_updateReview s1 cid uid p PID N rc
[PROOF STEP]
using eqExcPID_N_imp[OF ss1] u_defs
[PROOF STATE]
proof (prove)
using this:
e_updateReview s cid uid p PID N rc
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))
e_updateUser ?s ?uID ?p ?p' ?name ?info ?email \<equiv> IDsOK ?s [] [?uID] [] \<and> pass ?s ?uID = ?p
updateUser ?s ?uID ?p ?p' ?name ?info ?email \<equiv> ?s\<lparr>user := (user ?s)(?uID := User ?name ?info ?email), pass := (pass ?s)(?uID := ?p')\<rparr>
e_updateConfA ?s ?confID ?uID ?p \<equiv> IDsOK ?s [?confID] [?uID] [] \<and> pass ?s ?uID = ?p \<and> ?uID = voronkov ?s \<and> phase ?s ?confID = noPH
updateConfA ?s ?confID ?uID ?p \<equiv> ?s\<lparr>phase := (phase ?s)(?confID := setPH)\<rparr>
e_updatePhase ?s ?confID ?uID ?p ?ph \<equiv> IDsOK ?s [?confID] [?uID] [] \<and> pass ?s ?uID = ?p \<and> setPH \<le> phase ?s ?confID \<and> phase ?s ?confID < closedPH \<and> isChair ?s ?confID ?uID \<and> ?ph = SucPH (phase ?s ?confID)
updatePhase ?s ?confID ?uID ?p ?ph \<equiv> ?s\<lparr>phase := (phase ?s)(?confID := ?ph)\<rparr>
e_updatePaperTA ?s ?confID ?uID ?p ?papID ?name ?info \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> phase ?s ?confID = subPH \<and> isAut ?s ?confID ?uID ?papID
updatePaperTA ?s ?confID ?uID ?p ?papID ?title ?abstract \<equiv> case paper ?s ?papID of Paper title' abstract' pc reviews dis decs \<Rightarrow> ?s\<lparr>paper := (paper ?s)(?papID := Paper ?title ?abstract pc reviews dis decs)\<rparr>
e_updatePaperC ?s ?confID ?uID ?p ?papID ?pc \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> phase ?s ?confID = subPH \<and> isAut ?s ?confID ?uID ?papID
updatePaperC ?s ?confID ?uID ?p ?papID ?pc \<equiv> case paper ?s ?papID of Paper title abstract pc' reviews dis decs \<Rightarrow> ?s\<lparr>paper := (paper ?s)(?papID := Paper title abstract ?pc reviews dis decs)\<rparr>
e_updatePref ?s ?confID ?uID ?p ?papID ?pr \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> phase ?s ?confID = bidPH \<and> isPC ?s ?confID ?uID \<and> Aut ?papID \<notin> set (roles ?s ?confID ?uID)
updatePref ?s ?confID ?uID ?p ?papID ?pr \<equiv> ?s\<lparr>pref := fun_upd2 (pref ?s) ?uID ?papID ?pr\<rparr>
e_updateReview ?s ?confID ?uID ?p ?papID ?n ?rc \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> phase ?s ?confID = revPH \<and> isRev ?s ?confID ?uID ?papID \<and> getReviewIndex ?s ?confID ?uID ?papID = ?n
updateReview ?s ?confID ?uID ?p ?papID ?n ?rc \<equiv> case paper ?s ?papID of Paper title abstract pc reviews dis decs \<Rightarrow> let review = ?rc # emptyReview; reviews' = reviews[?n := review] in ?s\<lparr>paper := (paper ?s)(?papID := Paper title abstract pc reviews' dis decs)\<rparr>

goal (1 subgoal):
 1. e_updateReview s1 cid uid p PID N rc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e_updateReview s1 cid uid p PID N rc

goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
hence ou': "ou' = outOK"
[PROOF STATE]
proof (prove)
using this:
e_updateReview s1 cid uid p PID N rc

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

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

goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
let ?p = "paper s PID"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
let ?p1 = "paper s1 PID"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
have 1: "eqExcD ?p ?p1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcD (paper s PID) (paper s1 PID)
[PROOF STEP]
using ss1 eqExcPID_N_imp
[PROOF STATE]
proof (prove)
using this:
eqExcPID_N s s1
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. eqExcD (paper s PID) (paper s1 PID)
[PROOF STEP]
unfolding eeqExcPID_N_def
[PROOF STATE]
proof (prove)
using this:
eqExcPID_N s s1
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> (\<forall>pid. if pid = PID then eqExcD (paper ?s pid) (paper ?s1.0 pid) else paper ?s pid = paper ?s1.0 pid) \<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. eqExcD (paper s PID) (paper s1 PID)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eqExcD (paper s PID) (paper s1 PID)

goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
have 2: "reviewsPaper (paper s' PID) ! N = reviewsPaper (paper s1' PID) ! N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reviewsPaper (paper s' PID) ! N = reviewsPaper (paper s1' PID) ! N
[PROOF STEP]
using step step1[unfolded ou'] r r1
[PROOF STATE]
proof (prove)
using this:
step s a = (outOK, s')
step s1 a = (outOK, s1')
N < length (reviewsPaper (paper s PID))
N < length (reviewsPaper (paper s1 PID))

goal (1 subgoal):
 1. reviewsPaper (paper s' PID) ! N = reviewsPaper (paper s1' PID) ! N
[PROOF STEP]
unfolding a
[PROOF STATE]
proof (prove)
using this:
step s (Uact (uReview cid uid p PID N rc)) = (outOK, s')
step s1 (Uact (uReview cid uid p PID N rc)) = (outOK, s1')
N < length (reviewsPaper (paper s PID))
N < length (reviewsPaper (paper s1 PID))

goal (1 subgoal):
 1. reviewsPaper (paper s' PID) ! N = reviewsPaper (paper s1' PID) ! N
[PROOF STEP]
by (cases ?p, cases ?p1) (auto simp : u_defs)
[PROOF STATE]
proof (state)
this:
reviewsPaper (paper s' PID) ! N = reviewsPaper (paper s1' PID) ! N

goal (1 subgoal):
 1. \<exists>cid uid. isRevNth s cid uid PID N \<Longrightarrow> s' = s1'
[PROOF STEP]
from 1 2
[PROOF STATE]
proof (chain)
picking this:
eqExcD (paper s PID) (paper s1 PID)
reviewsPaper (paper s' PID) ! N = reviewsPaper (paper s1' PID) ! N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqExcD (paper s PID) (paper s1 PID)
reviewsPaper (paper s' PID) ! N = reviewsPaper (paper s1' PID) ! N

goal (1 subgoal):
 1. s' = s1'
[PROOF STEP]
using eqExcPID_N_imp_eq s's1'
[PROOF STATE]
proof (prove)
using this:
eqExcD (paper s PID) (paper s1 PID)
reviewsPaper (paper s' PID) ! N = reviewsPaper (paper s1' PID) ! N
\<lbrakk>eqExcPID_N ?s ?s1.0; reviewsPaper (paper ?s PID) ! N = reviewsPaper (paper ?s1.0 PID) ! N\<rbrakk> \<Longrightarrow> ?s = ?s1.0
eqExcPID_N s' s1'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma istate_\<Delta>1:
assumes B: "B vl vl1"
shows "\<Delta>1 istate vl istate vl1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>1 istate vl istate vl1
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
B vl vl1

goal (1 subgoal):
 1. \<Delta>1 istate vl istate vl1
[PROOF STEP]
unfolding \<Delta>1_def B_def istate_def
[PROOF STATE]
proof (prove)
using this:
\<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

goal (1 subgoal):
 1. (\<forall>cid. PID \<in>\<in> paperIDs \<lparr>confIDs = [], conf = \<lambda>confID. emptyConf, userIDs = [voronkovUserID], pass = \<lambda>uID. emptyPass, user = \<lambda>uID. emptyUser, roles = \<lambda>confID uID. [], paperIDs = \<lambda>confID. [], paper = \<lambda>papID. emptyPaper, pref = \<lambda>uID papID. NoPref, voronkov = voronkovUserID, news = \<lambda>confID. [], phase = \<lambda>confID. noPH\<rparr> cid \<longrightarrow> phase \<lparr>confIDs = [], conf = \<lambda>confID. emptyConf, userIDs = [voronkovUserID], pass = \<lambda>uID. emptyPass, user = \<lambda>uID. emptyUser, roles = \<lambda>confID uID. [], paperIDs = \<lambda>confID. [], paper = \<lambda>papID. emptyPaper, pref = \<lambda>uID papID. NoPref, voronkov = voronkovUserID, news = \<lambda>confID. [], phase = \<lambda>confID. noPH\<rparr> cid < revPH) \<and> \<lparr>confIDs = [], conf = \<lambda>confID. emptyConf, userIDs = [voronkovUserID], pass = \<lambda>uID. emptyPass, user = \<lambda>uID. emptyUser, roles = \<lambda>confID uID. [], paperIDs = \<lambda>confID. [], paper = \<lambda>papID. emptyPaper, pref = \<lambda>uID papID. NoPref, voronkov = voronkovUserID, news = \<lambda>confID. [], phase = \<lambda>confID. noPH\<rparr> = \<lparr>confIDs = [], conf = \<lambda>confID. emptyConf, userIDs = [voronkovUserID], pass = \<lambda>uID. emptyPass, user = \<lambda>uID. emptyUser, roles = \<lambda>confID uID. [], paperIDs = \<lambda>confID. [], paper = \<lambda>papID. emptyPaper, pref = \<lambda>uID papID. NoPref, voronkov = voronkovUserID, news = \<lambda>confID. [], phase = \<lambda>confID. noPH\<rparr> \<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


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

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>1 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
hence rs: "reach s" and ss1: "s1 = s" and B: "B vl vl1"
  and vl: "vl \<noteq> []" and vl1: "vl1 \<noteq> []" and PID_ph: "\<And> cid. PID \<in>\<in> paperIDs s cid \<longrightarrow> phase s cid < revPH"
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
\<Delta>1 s vl s1 vl1

goal (1 subgoal):
 1. (reach s &&& s1 = s &&& B vl vl1) &&& vl \<noteq> [] &&& vl1 \<noteq> [] &&& (\<And>cid. PID \<in>\<in> paperIDs s cid \<longrightarrow> phase s cid < revPH)
[PROOF STEP]
using reachNT_reach
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
\<Delta>1 s vl s1 vl1
reachNT ?s \<Longrightarrow> reach ?s

goal (1 subgoal):
 1. (reach s &&& s1 = s &&& B vl vl1) &&& vl \<noteq> [] &&& vl1 \<noteq> [] &&& (\<And>cid. PID \<in>\<in> paperIDs s cid \<longrightarrow> phase s cid < revPH)
[PROOF STEP]
unfolding \<Delta>1_def B_def
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
(\<forall>cid. PID \<in>\<in> paperIDs s cid \<longrightarrow> phase s cid < revPH) \<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. (reach s &&& 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> [] &&& (\<And>cid. PID \<in>\<in> paperIDs s cid \<longrightarrow> phase s cid < revPH)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reach s
s1 = s
B vl vl1
vl \<noteq> []
vl1 \<noteq> []
PID \<in>\<in> paperIDs s ?cid \<longrightarrow> phase s ?cid < revPH

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>1 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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 PID_ph
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
PID \<in>\<in> paperIDs s ?cid \<longrightarrow> 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]
by (fastforce simp: u_defs)+
[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 PID_ph
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
PID \<in>\<in> paperIDs s ?cid \<longrightarrow> 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]
by (fastforce simp: uu_defs)+
[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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s vl s1 vl1 \<or> \<Delta>2 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>1 s' vl' ?s1' ?vl1' \<or> \<Delta>2 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>1 s' vl' s' ?vl1' \<or> \<Delta>2 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>1 s' vl' s' ?vl1' \<or> \<Delta>2 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>1 s' vl' s' vl1 \<or> \<Delta>2 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>1 s' vl' s' vl1 \<or> \<Delta>2 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>1 s' vl' s' vl1 \<or> \<Delta>2 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>1 s' vl' s' vl1 \<or> \<Delta>2 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>1 s' vl' s' vl1 \<or> \<Delta>2 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>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 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>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
proof(cases "\<exists> cid. PID \<in>\<in> paperIDs s cid")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>cid. PID \<in>\<in> paperIDs s cid \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
 2. \<nexists>cid. PID \<in>\<in> paperIDs s cid \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>cid. PID \<in>\<in> paperIDs s cid

goal (2 subgoals):
 1. \<exists>cid. PID \<in>\<in> paperIDs s cid \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
 2. \<nexists>cid. PID \<in>\<in> paperIDs s cid \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
note PID = False
[PROOF STATE]
proof (state)
this:
\<nexists>cid. PID \<in>\<in> paperIDs s cid

goal (2 subgoals):
 1. \<exists>cid. PID \<in>\<in> paperIDs s cid \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
 2. \<nexists>cid. PID \<in>\<in> paperIDs s cid \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
have PID_ph': "\<And> cid. PID \<in>\<in> paperIDs s' cid \<Longrightarrow> phase s' cid < revPH"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cid. PID \<in>\<in> paperIDs s' cid \<Longrightarrow> phase s' cid < revPH
[PROOF STEP]
using PID step rs
[PROOF STATE]
proof (prove)
using this:
\<nexists>cid. PID \<in>\<in> paperIDs s cid
step s a = (ou, s')
reach s

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

goal (2 subgoals):
 1. \<exists>cid. PID \<in>\<in> paperIDs s cid \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
 2. \<nexists>cid. PID \<in>\<in> paperIDs s cid \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
hence "\<Delta>1 s' vl' s' vl1"
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> paperIDs s' ?cid \<Longrightarrow> phase s' ?cid < revPH

goal (1 subgoal):
 1. \<Delta>1 s' vl' s' vl1
[PROOF STEP]
unfolding \<Delta>1_def vl'
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> paperIDs s' ?cid \<Longrightarrow> phase s' ?cid < revPH

goal (1 subgoal):
 1. (\<forall>cid. PID \<in>\<in> paperIDs s' cid \<longrightarrow> phase s' cid < revPH) \<and> s' = s' \<and> B vl vl1
[PROOF STEP]
using B PID_ph' vl
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> paperIDs s' ?cid \<Longrightarrow> phase s' ?cid < revPH
B vl vl1
PID \<in>\<in> paperIDs s' ?cid \<Longrightarrow> phase s' ?cid < revPH
vl \<noteq> []

goal (1 subgoal):
 1. (\<forall>cid. PID \<in>\<in> paperIDs s' cid \<longrightarrow> phase s' cid < revPH) \<and> s' = s' \<and> B vl vl1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>1 s' vl' s' vl1

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

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

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

goal (1 subgoal):
 1. \<exists>cid. PID \<in>\<in> paperIDs s cid \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>cid. PID \<in>\<in> paperIDs s cid
[PROOF STEP]
obtain CID where PID: "PID \<in>\<in> paperIDs s CID"
[PROOF STATE]
proof (prove)
using this:
\<exists>cid. PID \<in>\<in> paperIDs s cid

goal (1 subgoal):
 1. (\<And>CID. PID \<in>\<in> paperIDs s CID \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
PID \<in>\<in> paperIDs s CID

goal (1 subgoal):
 1. \<exists>cid. PID \<in>\<in> paperIDs s cid \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
hence ph: "phase s CID < revPH"
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> paperIDs s CID

goal (1 subgoal):
 1. phase s CID < revPH
[PROOF STEP]
using PID_ph
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> paperIDs s CID
PID \<in>\<in> paperIDs s ?cid \<longrightarrow> 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. \<exists>cid. PID \<in>\<in> paperIDs s cid \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[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 PID paperIDs_mono step)
[PROOF STATE]
proof (state)
this:
PID \<in>\<in> paperIDs s' CID

goal (1 subgoal):
 1. \<exists>cid. PID \<in>\<in> paperIDs s cid \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
proof(cases "phase s' CID < revPH")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. phase s' CID < revPH \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
 2. \<not> phase s' CID < revPH \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 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>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
 2. \<not> phase s' CID < revPH \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 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>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
 2. \<not> phase s' CID < revPH \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
hence "\<Delta>1 s' vl' s' vl1"
[PROOF STATE]
proof (prove)
using this:
phase s' CID < revPH

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

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

goal (1 subgoal):
 1. (\<forall>cid. PID \<in>\<in> paperIDs s' cid \<longrightarrow> phase s' cid < revPH) \<and> s' = s' \<and> B vl vl1
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cid. \<lbrakk>B vl vl1; vl \<noteq> []; phase s' CID < revPH; PID \<in>\<in> paperIDs s' CID; PID \<in>\<in> paperIDs s' cid\<rbrakk> \<Longrightarrow> phase s' cid < revPH
[PROOF STEP]
by (metis reach_PairI paperIDs_equals rs step)
[PROOF STATE]
proof (state)
this:
\<Delta>1 s' vl' s' vl1

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

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

goal (1 subgoal):
 1. \<not> phase s' CID < revPH \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> phase s' CID < revPH \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> phase s' CID < revPH

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

goal (1 subgoal):
 1. \<not> phase s' CID < revPH \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
have "\<not> (\<exists> uid. isRevNth s CID uid PID N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>uid. isRevNth s CID uid PID N
[PROOF STEP]
using rs ph isRevNth_geq_revPH
[PROOF STATE]
proof (prove)
using this:
reach s
phase s CID < revPH
\<lbrakk>reach ?s; isRevNth ?s ?confID ?uID ?papID ?n\<rbrakk> \<Longrightarrow> revPH \<le> phase ?s ?confID

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

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

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

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

goal (1 subgoal):
 1. \<not> phase s' CID < revPH \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 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:
phase s' CID = revPH \<and> (\<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_imp_isRevNth reach_PairI rs step)
[PROOF STATE]
proof (state)
this:
\<nexists>uid. isREVNth s' uid PID N

goal (1 subgoal):
 1. \<not> phase s' CID < revPH \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 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 vl ph' PID' ph_isRev'
[PROOF STATE]
proof (prove)
using this:
\<nexists>uid. isREVNth s' uid PID N
B vl vl1
vl \<noteq> []
\<not> phase s' CID < revPH
PID \<in>\<in> paperIDs s' CID
phase s' CID = revPH \<and> (\<nexists>uid. isRevNth s' CID 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]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>2 s' vl' s' vl1

goal (1 subgoal):
 1. \<not> phase s' CID < revPH \<Longrightarrow> \<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 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>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>1 s' vl' s' vl1 \<or> \<Delta>2 s' vl' s' vl1 \<or> \<Delta>e s' vl' s' vl1

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

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

goal:
No subgoals!
[PROOF STEP]
qed