[STATEMENT]
lemma eqExcPID_step:
assumes s's1': "eqExcPID s s1"
and step: "step s a = (ou,s')"
and step1: "step s1 a = (ou1,s1')"
shows "eqExcPID s' s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID s' s1'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eqExcPID s' s1'
[PROOF STEP]
note eqs = eqExcPID_imp[OF s's1']
[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 (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

goal (1 subgoal):
 1. eqExcPID s' s1'
[PROOF STEP]
note eqs' = eqExcPID_imp1[OF s's1']
[PROOF STATE]
proof (state)
this:
eqExcD (paper s ?pid) (paper s1 ?pid)
?pid \<noteq> PID \<or> PID \<noteq> ?pid \<Longrightarrow> paper s ?pid = paper s1 ?pid \<and> getNthReview s ?pid ?n = getNthReview s1 ?pid ?n

goal (1 subgoal):
 1. eqExcPID s' s1'
[PROOF STEP]
note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID_def eeqExcPID_def eqExcD
[PROOF STATE]
proof (state)
this:
e_createUser ?s ?uID ?p ?name ?info ?email \<equiv> ?uID \<notin> set (userIDs ?s)
createUser ?s ?uID ?p ?name ?info ?email \<equiv> let uIDs = userIDs ?s in ?s\<lparr>userIDs := ?uID # uIDs, user := (user ?s)(?uID := User ?name ?info ?email), pass := (pass ?s)(?uID := ?p)\<rparr>
e_createConf ?s ?confID ?uID ?p ?name ?info \<equiv> IDsOK ?s [] [?uID] [] \<and> pass ?s ?uID = ?p \<and> ?confID \<notin> set (confIDs ?s)
createConf ?s ?confID ?uID ?p ?name ?info \<equiv> let confIDs = confIDs ?s in ?s\<lparr>confIDs := ?confID # confIDs, conf := (conf ?s)(?confID := Conf ?name ?info), roles := fun_upd2 (roles ?s) ?confID ?uID [PC, Chair]\<rparr>
e_createPC ?s ?confID ?uID ?p ?uID' \<equiv> let uIDs = userIDs ?s in IDsOK ?s [?confID] [?uID, ?uID'] [] \<and> pass ?s ?uID = ?p \<and> phase ?s ?confID = setPH \<and> isChair ?s ?confID ?uID
createPC ?s ?confID ?uID ?p ?uID' \<equiv> let rls = roles ?s ?confID ?uID' in ?s\<lparr>roles := fun_upd2 (roles ?s) ?confID ?uID' (List.insert PC rls)\<rparr>
e_createChair ?s ?confID ?uID ?p ?uID' \<equiv> let uIDs = userIDs ?s in IDsOK ?s [?confID] [?uID, ?uID'] [] \<and> pass ?s ?uID = ?p \<and> phase ?s ?confID = setPH \<and> isChair ?s ?confID ?uID
createChair ?s ?confID ?uID ?p ?uID' \<equiv> let rls = roles ?s ?confID ?uID' in ?s\<lparr>roles := fun_upd2 (roles ?s) ?confID ?uID' (List.insert PC (List.insert Chair rls))\<rparr>
e_createAuthor ?s ?confID ?uID ?p ?papID ?uID' \<equiv> IDsOK ?s [?confID] [?uID, ?uID'] [?papID] \<and> pass ?s ?uID = ?p \<and> phase ?s ?confID = subPH \<and> isAut ?s ?confID ?uID ?papID \<and> ?uID \<noteq> ?uID'
createAuthor ?s ?confID ?uID ?p ?papID ?uID' \<equiv> let rls = roles ?s ?confID ?uID' in ?s\<lparr>roles := fun_upd2 (roles ?s) ?confID ?uID' (List.insert (Aut ?papID) rls), pref := fun_upd2 (pref ?s) ?uID' ?papID Conflict\<rparr>
e_createConflict ?s ?confID ?uID ?p ?papID ?uID' \<equiv> IDsOK ?s [?confID] [?uID, ?uID'] [?papID] \<and> pass ?s ?uID = ?p \<and> phase ?s ?confID = subPH \<and> isAut ?s ?confID ?uID ?papID \<and> isPC ?s ?confID ?uID'
createConflict ?s ?confID ?uID ?p ?papID ?uID' \<equiv> ?s\<lparr>pref := fun_upd2 (pref ?s) ?uID' ?papID Conflict\<rparr>
e_createPaper ?s ?confID ?uID ?p ?papID ?name ?info \<equiv> IDsOK ?s [?confID] [?uID] [] \<and> pass ?s ?uID = ?p \<and> phase ?s ?confID = subPH \<and> ?papID \<notin> set (getAllPaperIDs ?s)
createPaper ?s ?confID ?uID ?p ?papID ?title ?abstract \<equiv> let papIDs = paperIDs ?s ?confID; rls = roles ?s ?confID ?uID in ?s\<lparr>paperIDs := (paperIDs ?s)(?confID := ?papID # papIDs), paper := (paper ?s)(?papID := Paper ?title ?abstract NoPContent [] (Dis []) []), roles := fun_upd2 (roles ?s) ?confID ?uID (List.insert (Aut ?papID) rls), pref := fun_upd2 (pref ?s) ?uID ?papID Conflict\<rparr>
e_createReview ?s ?confID ?uID ?p ?papID ?uID' \<equiv> IDsOK ?s [?confID] [?uID, ?uID'] [?papID] \<and> pass ?s ?uID = ?p \<and> phase ?s ?confID = revPH \<and> isChair ?s ?confID ?uID \<and> pref ?s ?uID ?papID \<noteq> Conflict \<and> isPC ?s ?confID ?uID' \<and> \<not> isRev ?s ?confID ?uID' ?papID \<and> pref ?s ?uID' ?papID \<noteq> Conflict
createReview ?s ?confID ?uID ?p ?papID ?uID' \<equiv> case paper ?s ?papID of Paper title abstract pc reviews dis decs \<Rightarrow> let rls = roles ?s ?confID ?uID'; n = length (reviewsPaper (paper ?s ?papID)); reviews' = reviews ## emptyReview in ?s\<lparr>roles := fun_upd2 (roles ?s) ?confID ?uID' (List.insert (Rev ?papID n) rls), paper := (paper ?s)(?papID := Paper title abstract pc reviews' dis decs)\<rparr>
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>
e_uupdateNews ?s ?confID ?uID ?p ?ev \<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
uupdateNews ?s ?confID ?uID ?p ?ev \<equiv> let evs = news ?s ?confID in ?s\<lparr>news := (news ?s)(?confID := ?ev # evs)\<rparr>
e_uupdateDis ?s ?confID ?uID ?p ?papID ?comm \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> phase ?s ?confID = disPH \<and> isPC ?s ?confID ?uID \<and> pref ?s ?uID ?papID \<noteq> Conflict
uupdateDis ?s ?confID ?uID ?p ?papID ?comm \<equiv> case paper ?s ?papID of Paper title abstract pc reviews (Dis comments) decs \<Rightarrow> ?s\<lparr>paper := (paper ?s)(?papID := Paper title abstract pc reviews (Dis (?comm # comments)) decs)\<rparr>
e_uupdateReview ?s ?confID ?uID ?p ?papID ?n ?rc \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> phase ?s ?confID = disPH \<and> isRev ?s ?confID ?uID ?papID \<and> getReviewIndex ?s ?confID ?uID ?papID = ?n
uupdateReview ?s ?confID ?uID ?p ?papID ?n ?rc \<equiv> case paper ?s ?papID of Paper title abstract pc reviews dis decs \<Rightarrow> let review = ?rc # reviews ! ?n; reviews' = reviews[?n := review] in ?s\<lparr>paper := (paper ?s)(?papID := Paper title abstract pc reviews' dis decs)\<rparr>
uupdateDec ?s ?confID ?uID ?p ?papID ?dec \<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 (?dec # decs))\<rparr>
e_uupdateDec ?s ?confID ?uID ?p ?papID ?dec \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> phase ?s ?confID = disPH \<and> isChair ?s ?confID ?uID \<and> pref ?s ?uID ?papID \<noteq> Conflict
readAmIVoronkov ?s ?uID ?p \<equiv> ?uID = voronkov ?s
e_readAmIVoronkov ?s ?uID ?p \<equiv> IDsOK ?s [] [?uID] [] \<and> pass ?s ?uID = ?p
readUser ?s ?uID ?p ?uID' \<equiv> case user ?s ?uID' of User name info email \<Rightarrow> (name, info, email)
e_readUser ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [] [?uID, ?uID'] [] \<and> pass ?s ?uID = ?p
readConf ?s ?confID ?uID ?p \<equiv> (nameConf (conf ?s ?confID), infoConf (conf ?s ?confID), filter (\<lambda>rl. \<not> isRevRole rl) (roles ?s ?confID ?uID), phase ?s ?confID)
e_readConf ?s ?confID ?uID ?p \<equiv> IDsOK ?s [?confID] [?uID] [] \<and> pass ?s ?uID = ?p
readNews ?s ?confID ?uID ?p \<equiv> news ?s ?confID
e_readNews ?s ?confID ?uID ?p \<equiv> IDsOK ?s [?confID] [?uID] [] \<and> pass ?s ?uID = ?p \<and> setPH \<le> phase ?s ?confID \<and> isPC ?s ?confID ?uID
readPaperTAA ?s ?confID ?uID ?p ?papID \<equiv> case paper ?s ?papID of Paper title abstract pc reviews dis decs \<Rightarrow> (title, abstract, cmap (\<lambda>uID. if isAut ?s ?confID uID ?papID then [uID] else []) (userIDs ?s))
e_readPaperTAA ?s ?confID ?uID ?p ?papID \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> subPH \<le> phase ?s ?confID \<and> (isAut ?s ?confID ?uID ?papID \<or> isPC ?s ?confID ?uID)
readPaperC ?s ?confID ?uID ?p ?papID \<equiv> case paper ?s ?papID of Paper title abstract pc reviews dis decs \<Rightarrow> pc
e_readPaperC ?s ?confID ?uID ?p ?papID \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> (subPH \<le> phase ?s ?confID \<and> isAut ?s ?confID ?uID ?papID \<or> bidPH \<le> phase ?s ?confID \<and> isPC ?s ?confID ?uID)
readPref ?s ?confID ?uID ?p ?papID \<equiv> pref ?s ?uID ?papID
e_readPref ?s ?confID ?uID ?p ?papID \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> bidPH \<le> phase ?s ?confID \<and> isPC ?s ?confID ?uID
readMyReview ?s ?confID ?uID ?p ?papID \<equiv> case getRevRole ?s ?confID ?uID ?papID of Some (Rev papID' n) \<Rightarrow> (n, getNthReview ?s ?papID n)
e_readMyReview ?s ?confID ?uID ?p ?papID \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> revPH \<le> phase ?s ?confID \<and> isRev ?s ?confID ?uID ?papID
readReviews ?s ?confID ?uID ?p ?papID \<equiv> getReviewersReviews ?s ?confID ?papID
e_readReviews ?s ?confID ?uID ?p ?papID \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> disPH \<le> phase ?s ?confID \<and> isPC ?s ?confID ?uID \<and> pref ?s ?uID ?papID \<noteq> Conflict
readDecs ?s ?confID ?uID ?p ?papID \<equiv> case paper ?s ?papID of Paper title abstract pc reviews dis decs \<Rightarrow> decs
e_readDecs ?s ?confID ?uID ?p ?papID \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> disPH \<le> phase ?s ?confID \<and> isPC ?s ?confID ?uID \<and> pref ?s ?uID ?papID \<noteq> Conflict
readDis ?s ?confID ?uID ?p ?papID \<equiv> case paper ?s ?papID of Paper title abstract pc reviews (Dis comments) decs \<Rightarrow> comments
e_readDis ?s ?confID ?uID ?p ?papID \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> disPH \<le> phase ?s ?confID \<and> isPC ?s ?confID ?uID \<and> pref ?s ?uID ?papID \<noteq> Conflict
readFinalReviews ?s ?confID ?uID ?p ?papID \<equiv> map (\<lambda>rev. case rev of [] \<Rightarrow> (NoExp, NoScore, emptyStr) # emptyReview | (exp, score, comm) # rv \<Rightarrow> (exp, score, comm) # emptyReview) (reviewsPaper (paper ?s ?papID))
e_readFinalReviews ?s ?confID ?uID ?p ?papID \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> notifPH \<le> phase ?s ?confID \<and> (isAut ?s ?confID ?uID ?papID \<or> isPC ?s ?confID ?uID \<and> pref ?s ?uID ?papID \<noteq> Conflict)
readFinalDec ?s ?confID ?uID ?p ?papID \<equiv> case paper ?s ?papID of Paper title abstract pc reviews dis [] \<Rightarrow> NoDecision | Paper title abstract pc reviews dis (dec # decsa) \<Rightarrow> dec
e_readFinalDec ?s ?confID ?uID ?p ?papID \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> notifPH \<le> phase ?s ?confID \<and> (isAut ?s ?confID ?uID ?papID \<or> isPC ?s ?confID ?uID)
readPrefOfPC ?s ?confID ?uID ?p ?papID ?uID' \<equiv> pref ?s ?uID' ?papID
e_readPrefOfPC ?s ?confID ?uID ?p ?papID ?uID' \<equiv> IDsOK ?s [?confID] [?uID, ?uID'] [?papID] \<and> pass ?s ?uID = ?p \<and> (bidPH \<le> phase ?s ?confID \<and> isChair ?s ?confID ?uID \<and> isPC ?s ?confID ?uID' \<or> phase ?s ?confID = subPH \<and> isAut ?s ?confID ?uID ?papID)
listConfs ?s ?uID ?p \<equiv> confIDs ?s
e_listConfs ?s ?uID ?p \<equiv> IDsOK ?s [] [?uID] [] \<and> pass ?s ?uID = ?p \<and> ?uID = voronkov ?s
listAConfs ?s ?uID ?p \<equiv> cmap (\<lambda>confID. if phase ?s confID = noPH then [confID] else []) (confIDs ?s)
e_listAConfs ?s ?uID ?p \<equiv> IDsOK ?s [] [?uID] [] \<and> pass ?s ?uID = ?p \<and> ?uID = voronkov ?s
listSConfs ?s ?uID ?p \<equiv> cmap (\<lambda>confID. if phase ?s confID = subPH then [confID] else []) (confIDs ?s)
e_listSConfs ?s ?uID ?p \<equiv> IDsOK ?s [] [?uID] [] \<and> pass ?s ?uID = ?p
listMyConfs ?s ?uID ?p \<equiv> cmap (\<lambda>confID. if roles ?s confID ?uID \<noteq> [] then [confID] else []) (confIDs ?s)
e_listMyConfs ?s ?uID ?p \<equiv> IDsOK ?s [] [?uID] [] \<and> pass ?s ?uID = ?p
listAllUsers ?s ?uID ?p \<equiv> userIDs ?s
e_listAllUsers ?s ?uID ?p \<equiv> IDsOK ?s [] [?uID] [] \<and> pass ?s ?uID = ?p
listAllPapers ?s ?uID ?p \<equiv> getAllPaperIDs ?s
e_listAllPapers ?s ?uID ?p \<equiv> IDsOK ?s [] [?uID] [] \<and> pass ?s ?uID = ?p
listPC ?s ?confID ?uID ?p \<equiv> cmap (\<lambda>uID. if isPC ?s ?confID uID then [uID] else []) (userIDs ?s)
e_listPC ?s ?confID ?uID ?p \<equiv> IDsOK ?s [?confID] [?uID] [] \<and> pass ?s ?uID = ?p \<and> (subPH \<le> phase ?s ?confID \<or> setPH \<le> phase ?s ?confID \<and> isChair ?s ?confID ?uID)
listChair ?s ?confID ?uID ?p \<equiv> cmap (\<lambda>uID. if isChair ?s ?confID uID then [uID] else []) (userIDs ?s)
e_listChair ?s ?confID ?uID ?p \<equiv> IDsOK ?s [?confID] [?uID] [] \<and> pass ?s ?uID = ?p \<and> (subPH \<le> phase ?s ?confID \<or> setPH \<le> phase ?s ?confID \<and> isChair ?s ?confID ?uID)
listPapers ?s ?confID ?uID ?p \<equiv> let paps = paper ?s in map (\<lambda>papID. papID) (paperIDs ?s ?confID)
e_listPapers ?s ?confID ?uID ?p \<equiv> IDsOK ?s [?confID] [?uID] [] \<and> pass ?s ?uID = ?p \<and> subPH \<le> phase ?s ?confID \<and> isPC ?s ?confID ?uID
listMyPapers ?s ?confID ?uID ?p \<equiv> let paps = paper ?s in cmap (\<lambda>papID. if isAut ?s ?confID ?uID papID then [papID] else []) (paperIDs ?s ?confID)
e_listMyPapers ?s ?confID ?uID ?p \<equiv> IDsOK ?s [?confID] [?uID] [] \<and> pass ?s ?uID = ?p \<and> subPH \<le> phase ?s ?confID
listMyAssignedPapers ?s ?confID ?uID ?p \<equiv> let paps = paper ?s in cmap (\<lambda>papID. if isRev ?s ?confID ?uID papID then [papID] else []) (paperIDs ?s ?confID)
e_listMyAssignedPapers ?s ?confID ?uID ?p \<equiv> IDsOK ?s [?confID] [?uID] [] \<and> pass ?s ?uID = ?p \<and> revPH \<le> phase ?s ?confID \<and> isPC ?s ?confID ?uID
listAssignedReviewers ?s ?confID ?uID ?p ?papID \<equiv> filter (\<lambda>uID. isRev ?s ?confID uID ?papID) (userIDs ?s)
e_listAssignedReviewers ?s ?confID ?uID ?p ?papID \<equiv> IDsOK ?s [?confID] [?uID] [?papID] \<and> pass ?s ?uID = ?p \<and> revPH \<le> phase ?s ?confID \<and> isChair ?s ?confID ?uID \<and> pref ?s ?uID ?papID \<noteq> Conflict
(?p = Paper ?title ?abstract ?content ?reviews ?dis ?decs) = (?title = titlePaper ?p \<and> ?abstract = abstractPaper ?p \<and> ?content = contentPaper ?p \<and> ?reviews = reviewsPaper ?p \<and> ?dis = disPaper ?p \<and> ?decs = decsPaper ?p)
eqExcPID ?s ?s1.0 \<equiv> 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 (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
eeqExcPID ?paps ?paps1.0 \<equiv> \<forall>pid. if pid = PID then eqExcD (?paps pid) (?paps1.0 pid) else ?paps pid = ?paps1.0 pid
eqExcD ?pap ?pap1.0 = (titlePaper ?pap = titlePaper ?pap1.0 \<and> abstractPaper ?pap = abstractPaper ?pap1.0 \<and> contentPaper ?pap = contentPaper ?pap1.0 \<and> reviewsPaper ?pap = reviewsPaper ?pap1.0 \<and> disPaper ?pap = disPaper ?pap1.0)

goal (1 subgoal):
 1. eqExcPID s' s1'
[PROOF STEP]
note * = step step1 eqs eqs'
[PROOF STATE]
proof (state)
this:
step s a = (ou, s')
step s1 a = (ou1, 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 (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
eqExcD (paper s ?pid) (paper s1 ?pid)
?pid \<noteq> PID \<or> PID \<noteq> ?pid \<Longrightarrow> paper s ?pid = paper s1 ?pid \<and> getNthReview s ?pid ?n = getNthReview s1 ?pid ?n

goal (1 subgoal):
 1. eqExcPID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
step s a = (ou, s')
step s1 a = (ou1, 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 (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
eqExcD (paper s ?pid) (paper s1 ?pid)
?pid \<noteq> PID \<or> PID \<noteq> ?pid \<Longrightarrow> paper s ?pid = paper s1 ?pid \<and> getNthReview s ?pid ?n = getNthReview s1 ?pid ?n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
step s1 a = (ou1, 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 (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
eqExcD (paper s ?pid) (paper s1 ?pid)
?pid \<noteq> PID \<or> PID \<noteq> ?pid \<Longrightarrow> paper s ?pid = paper s1 ?pid \<and> getNthReview s ?pid ?n = getNthReview s1 ?pid ?n

goal (1 subgoal):
 1. eqExcPID s' s1'
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Cact x1\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 2. \<And>x2. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Uact x2\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 3. \<And>x3. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = UUact x3\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 4. \<And>x4. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Ract x4\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 5. \<And>x5. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Lact x5\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
[PROOF STEP]
case (Cact x1)
[PROOF STATE]
proof (state)
this:
a = Cact x1

goal (5 subgoals):
 1. \<And>x1. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Cact x1\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 2. \<And>x2. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Uact x2\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 3. \<And>x3. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = UUact x3\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 4. \<And>x4. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Ract x4\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 5. \<And>x5. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Lact x5\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Cact x1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Cact x1

goal (1 subgoal):
 1. eqExcPID s' s1'
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
a = Cact x1
step s a = (ou, s')
step s1 a = (ou1, 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 (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
eqExcD (paper s ?pid) (paper s1 ?pid)
?pid \<noteq> PID \<or> PID \<noteq> ?pid \<Longrightarrow> paper s ?pid = paper s1 ?pid \<and> getNthReview s ?pid ?n = getNthReview s1 ?pid ?n

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

goal (4 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Uact x2\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = UUact x3\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 3. \<And>x4. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Ract x4\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 4. \<And>x5. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Lact x5\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Uact x2\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = UUact x3\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 3. \<And>x4. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Ract x4\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 4. \<And>x5. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Lact x5\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
[PROOF STEP]
case (Uact x2)
[PROOF STATE]
proof (state)
this:
a = Uact x2

goal (4 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Uact x2\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = UUact x3\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 3. \<And>x4. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Ract x4\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 4. \<And>x5. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Lact x5\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Uact x2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Uact x2

goal (1 subgoal):
 1. eqExcPID s' s1'
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
a = Uact x2
step s a = (ou, s')
step s1 a = (ou1, 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 (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
eqExcD (paper s ?pid) (paper s1 ?pid)
?pid \<noteq> PID \<or> PID \<noteq> ?pid \<Longrightarrow> paper s ?pid = paper s1 ?pid \<and> getNthReview s ?pid ?n = getNthReview s1 ?pid ?n

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

goal (3 subgoals):
 1. \<And>x3. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = UUact x3\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 2. \<And>x4. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Ract x4\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Lact x5\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = UUact x3\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 2. \<And>x4. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Ract x4\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Lact x5\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
[PROOF STEP]
case (UUact x3)
[PROOF STATE]
proof (state)
this:
a = UUact x3

goal (3 subgoals):
 1. \<And>x3. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = UUact x3\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 2. \<And>x4. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Ract x4\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Lact x5\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = UUact x3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = UUact x3

goal (1 subgoal):
 1. eqExcPID s' s1'
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
a = UUact x3
step s a = (ou, s')
step s1 a = (ou1, 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 (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
eqExcD (paper s ?pid) (paper s1 ?pid)
?pid \<noteq> PID \<or> PID \<noteq> ?pid \<Longrightarrow> paper s ?pid = paper s1 ?pid \<and> getNthReview s ?pid ?n = getNthReview s1 ?pid ?n

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

goal (2 subgoals):
 1. \<And>x4. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Ract x4\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
 2. \<And>x5. \<lbrakk>step s a = (ou, s'); step s1 a = (ou1, s1'); \<And>cid uid pid. 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 (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>pid. eqExcD (paper s pid) (paper s1 pid); \<And>pid n. pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n; a = Lact x5\<rbrakk> \<Longrightarrow> eqExcPID s' s1'
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
eqExcPID s' s1'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqExcPID_step_\<phi>_imp:
assumes s's1': "eqExcPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and \<phi>: "\<phi> (Trans s a ou s')"
shows "\<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqExcPID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
\<phi> (Trans s a ou s')

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
unfolding \<phi>_def2
[PROOF STATE]
proof (prove)
using this:
eqExcPID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK

goal (1 subgoal):
 1. \<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou1 = outOK
[PROOF STEP]
by (auto simp add: uu_defs eqExcPID_imp)


[STATEMENT]
lemma eqExcPID_step_\<phi>:
assumes s's1': "eqExcPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
shows "\<phi> (Trans s a ou s') = \<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s a ou s') = \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
by (metis eqExcPID_step_\<phi>_imp eqExcPID_sym assms)