[STATEMENT]
lemma eqExcPID_imp2:
assumes "eqExcPID s s1" and "pid \<noteq> PID \<or> PID \<noteq> pid"
shows "getReviewersReviews s cid pid = getReviewersReviews s1 cid pid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getReviewersReviews s cid pid = getReviewersReviews s1 cid pid
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. getReviewersReviews s cid pid = getReviewersReviews s1 cid pid
[PROOF STEP]
have
  "(\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) =
   (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uID. (if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqExcPID s s1
pid \<noteq> PID \<or> PID \<noteq> pid

goal (1 subgoal):
 1. \<And>uID. (if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])
[PROOF STEP]
by (auto simp: eqExcPID_imp eqExcPID_imp1)
[PROOF STATE]
proof (state)
this:
(\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])

goal (1 subgoal):
 1. getReviewersReviews s cid pid = getReviewersReviews s1 cid pid
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])

goal (1 subgoal):
 1. getReviewersReviews s cid pid = getReviewersReviews s1 cid pid
[PROOF STEP]
unfolding getReviewersReviews_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])

goal (1 subgoal):
 1. cmap (\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) (userIDs s) = cmap (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else []) (userIDs s1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])
eqExcPID s s1
pid \<noteq> PID \<or> PID \<noteq> pid

goal (1 subgoal):
 1. cmap (\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) (userIDs s) = cmap (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else []) (userIDs s1)
[PROOF STEP]
by (simp add: eqExcPID_imp)
[PROOF STATE]
proof (state)
this:
getReviewersReviews s cid pid = getReviewersReviews s1 cid pid

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqExcPID_cong[simp, intro]:
"\<And> uu1 uu2. eqExcPID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID (s \<lparr>confIDs := uu1\<rparr>) (s1 \<lparr>confIDs := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID (s \<lparr>conf := uu1\<rparr>) (s1 \<lparr>conf := uu2\<rparr>)"

"\<And> uu1 uu2. eqExcPID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID (s \<lparr>userIDs := uu1\<rparr>) (s1 \<lparr>userIDs := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID (s \<lparr>pass := uu1\<rparr>) (s1 \<lparr>pass := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID (s \<lparr>user := uu1\<rparr>) (s1 \<lparr>user := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID (s \<lparr>roles := uu1\<rparr>) (s1 \<lparr>roles := uu2\<rparr>)"

"\<And> uu1 uu2. eqExcPID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID (s \<lparr>paperIDs := uu1\<rparr>) (s1 \<lparr>paperIDs := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID s s1 \<Longrightarrow> eeqExcPID uu1 uu2 \<Longrightarrow> eqExcPID (s \<lparr>paper := uu1\<rparr>) (s1 \<lparr>paper := uu2\<rparr>)"

"\<And> uu1 uu2. eqExcPID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID (s \<lparr>pref := uu1\<rparr>) (s1 \<lparr>pref := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID (s \<lparr>voronkov := uu1\<rparr>) (s1 \<lparr>voronkov := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID (s \<lparr>news := uu1\<rparr>) (s1 \<lparr>news := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID (s \<lparr>phase := uu1\<rparr>) (s1 \<lparr>phase := uu2\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<And>uu1 uu2. \<lbrakk>eqExcPID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID (s\<lparr>confIDs := uu1\<rparr>) (s1\<lparr>confIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID (s\<lparr>conf := uu1\<rparr>) (s1\<lparr>conf := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID (s\<lparr>userIDs := uu1\<rparr>) (s1\<lparr>userIDs := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID (s\<lparr>pass := uu1\<rparr>) (s1\<lparr>pass := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID (s\<lparr>user := uu1\<rparr>) (s1\<lparr>user := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID (s\<lparr>roles := uu1\<rparr>) (s1\<lparr>roles := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>eqExcPID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID (s\<lparr>paperIDs := uu1\<rparr>) (s1\<lparr>paperIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID s s1; eeqExcPID uu1 uu2\<rbrakk> \<Longrightarrow> eqExcPID (s\<lparr>paper := uu1\<rparr>) (s1\<lparr>paper := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID (s\<lparr>pref := uu1\<rparr>) (s1\<lparr>pref := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID (s\<lparr>voronkov := uu1\<rparr>) (s1\<lparr>voronkov := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID (s\<lparr>news := uu1\<rparr>) (s1\<lparr>news := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID (s\<lparr>phase := uu1\<rparr>) (s1\<lparr>phase := uu2\<rparr>))
[PROOF STEP]
unfolding eqExcPID_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<And>uu1 uu2. \<lbrakk>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; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>confIDs := uu1\<rparr>) = confIDs (s1\<lparr>confIDs := uu2\<rparr>) \<and> conf (s\<lparr>confIDs := uu1\<rparr>) = conf (s1\<lparr>confIDs := uu2\<rparr>) \<and> userIDs (s\<lparr>confIDs := uu1\<rparr>) = userIDs (s1\<lparr>confIDs := uu2\<rparr>) \<and> pass (s\<lparr>confIDs := uu1\<rparr>) = pass (s1\<lparr>confIDs := uu2\<rparr>) \<and> user (s\<lparr>confIDs := uu1\<rparr>) = user (s1\<lparr>confIDs := uu2\<rparr>) \<and> roles (s\<lparr>confIDs := uu1\<rparr>) = roles (s1\<lparr>confIDs := uu2\<rparr>) \<and> paperIDs (s\<lparr>confIDs := uu1\<rparr>) = paperIDs (s1\<lparr>confIDs := uu2\<rparr>) \<and> eeqExcPID (paper (s\<lparr>confIDs := uu1\<rparr>)) (paper (s1\<lparr>confIDs := uu2\<rparr>)) \<and> pref (s\<lparr>confIDs := uu1\<rparr>) = pref (s1\<lparr>confIDs := uu2\<rparr>) \<and> voronkov (s\<lparr>confIDs := uu1\<rparr>) = voronkov (s1\<lparr>confIDs := uu2\<rparr>) \<and> news (s\<lparr>confIDs := uu1\<rparr>) = news (s1\<lparr>confIDs := uu2\<rparr>) \<and> phase (s\<lparr>confIDs := uu1\<rparr>) = phase (s1\<lparr>confIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>conf := uu1\<rparr>) = confIDs (s1\<lparr>conf := uu2\<rparr>) \<and> conf (s\<lparr>conf := uu1\<rparr>) = conf (s1\<lparr>conf := uu2\<rparr>) \<and> userIDs (s\<lparr>conf := uu1\<rparr>) = userIDs (s1\<lparr>conf := uu2\<rparr>) \<and> pass (s\<lparr>conf := uu1\<rparr>) = pass (s1\<lparr>conf := uu2\<rparr>) \<and> user (s\<lparr>conf := uu1\<rparr>) = user (s1\<lparr>conf := uu2\<rparr>) \<and> roles (s\<lparr>conf := uu1\<rparr>) = roles (s1\<lparr>conf := uu2\<rparr>) \<and> paperIDs (s\<lparr>conf := uu1\<rparr>) = paperIDs (s1\<lparr>conf := uu2\<rparr>) \<and> eeqExcPID (paper (s\<lparr>conf := uu1\<rparr>)) (paper (s1\<lparr>conf := uu2\<rparr>)) \<and> pref (s\<lparr>conf := uu1\<rparr>) = pref (s1\<lparr>conf := uu2\<rparr>) \<and> voronkov (s\<lparr>conf := uu1\<rparr>) = voronkov (s1\<lparr>conf := uu2\<rparr>) \<and> news (s\<lparr>conf := uu1\<rparr>) = news (s1\<lparr>conf := uu2\<rparr>) \<and> phase (s\<lparr>conf := uu1\<rparr>) = phase (s1\<lparr>conf := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>userIDs := uu1\<rparr>) = confIDs (s1\<lparr>userIDs := uu2\<rparr>) \<and> conf (s\<lparr>userIDs := uu1\<rparr>) = conf (s1\<lparr>userIDs := uu2\<rparr>) \<and> userIDs (s\<lparr>userIDs := uu1\<rparr>) = userIDs (s1\<lparr>userIDs := uu2\<rparr>) \<and> pass (s\<lparr>userIDs := uu1\<rparr>) = pass (s1\<lparr>userIDs := uu2\<rparr>) \<and> user (s\<lparr>userIDs := uu1\<rparr>) = user (s1\<lparr>userIDs := uu2\<rparr>) \<and> roles (s\<lparr>userIDs := uu1\<rparr>) = roles (s1\<lparr>userIDs := uu2\<rparr>) \<and> paperIDs (s\<lparr>userIDs := uu1\<rparr>) = paperIDs (s1\<lparr>userIDs := uu2\<rparr>) \<and> eeqExcPID (paper (s\<lparr>userIDs := uu1\<rparr>)) (paper (s1\<lparr>userIDs := uu2\<rparr>)) \<and> pref (s\<lparr>userIDs := uu1\<rparr>) = pref (s1\<lparr>userIDs := uu2\<rparr>) \<and> voronkov (s\<lparr>userIDs := uu1\<rparr>) = voronkov (s1\<lparr>userIDs := uu2\<rparr>) \<and> news (s\<lparr>userIDs := uu1\<rparr>) = news (s1\<lparr>userIDs := uu2\<rparr>) \<and> phase (s\<lparr>userIDs := uu1\<rparr>) = phase (s1\<lparr>userIDs := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>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; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>pass := uu1\<rparr>) = confIDs (s1\<lparr>pass := uu2\<rparr>) \<and> conf (s\<lparr>pass := uu1\<rparr>) = conf (s1\<lparr>pass := uu2\<rparr>) \<and> userIDs (s\<lparr>pass := uu1\<rparr>) = userIDs (s1\<lparr>pass := uu2\<rparr>) \<and> pass (s\<lparr>pass := uu1\<rparr>) = pass (s1\<lparr>pass := uu2\<rparr>) \<and> user (s\<lparr>pass := uu1\<rparr>) = user (s1\<lparr>pass := uu2\<rparr>) \<and> roles (s\<lparr>pass := uu1\<rparr>) = roles (s1\<lparr>pass := uu2\<rparr>) \<and> paperIDs (s\<lparr>pass := uu1\<rparr>) = paperIDs (s1\<lparr>pass := uu2\<rparr>) \<and> eeqExcPID (paper (s\<lparr>pass := uu1\<rparr>)) (paper (s1\<lparr>pass := uu2\<rparr>)) \<and> pref (s\<lparr>pass := uu1\<rparr>) = pref (s1\<lparr>pass := uu2\<rparr>) \<and> voronkov (s\<lparr>pass := uu1\<rparr>) = voronkov (s1\<lparr>pass := uu2\<rparr>) \<and> news (s\<lparr>pass := uu1\<rparr>) = news (s1\<lparr>pass := uu2\<rparr>) \<and> phase (s\<lparr>pass := uu1\<rparr>) = phase (s1\<lparr>pass := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>user := uu1\<rparr>) = confIDs (s1\<lparr>user := uu2\<rparr>) \<and> conf (s\<lparr>user := uu1\<rparr>) = conf (s1\<lparr>user := uu2\<rparr>) \<and> userIDs (s\<lparr>user := uu1\<rparr>) = userIDs (s1\<lparr>user := uu2\<rparr>) \<and> pass (s\<lparr>user := uu1\<rparr>) = pass (s1\<lparr>user := uu2\<rparr>) \<and> user (s\<lparr>user := uu1\<rparr>) = user (s1\<lparr>user := uu2\<rparr>) \<and> roles (s\<lparr>user := uu1\<rparr>) = roles (s1\<lparr>user := uu2\<rparr>) \<and> paperIDs (s\<lparr>user := uu1\<rparr>) = paperIDs (s1\<lparr>user := uu2\<rparr>) \<and> eeqExcPID (paper (s\<lparr>user := uu1\<rparr>)) (paper (s1\<lparr>user := uu2\<rparr>)) \<and> pref (s\<lparr>user := uu1\<rparr>) = pref (s1\<lparr>user := uu2\<rparr>) \<and> voronkov (s\<lparr>user := uu1\<rparr>) = voronkov (s1\<lparr>user := uu2\<rparr>) \<and> news (s\<lparr>user := uu1\<rparr>) = news (s1\<lparr>user := uu2\<rparr>) \<and> phase (s\<lparr>user := uu1\<rparr>) = phase (s1\<lparr>user := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>roles := uu1\<rparr>) = confIDs (s1\<lparr>roles := uu2\<rparr>) \<and> conf (s\<lparr>roles := uu1\<rparr>) = conf (s1\<lparr>roles := uu2\<rparr>) \<and> userIDs (s\<lparr>roles := uu1\<rparr>) = userIDs (s1\<lparr>roles := uu2\<rparr>) \<and> pass (s\<lparr>roles := uu1\<rparr>) = pass (s1\<lparr>roles := uu2\<rparr>) \<and> user (s\<lparr>roles := uu1\<rparr>) = user (s1\<lparr>roles := uu2\<rparr>) \<and> roles (s\<lparr>roles := uu1\<rparr>) = roles (s1\<lparr>roles := uu2\<rparr>) \<and> paperIDs (s\<lparr>roles := uu1\<rparr>) = paperIDs (s1\<lparr>roles := uu2\<rparr>) \<and> eeqExcPID (paper (s\<lparr>roles := uu1\<rparr>)) (paper (s1\<lparr>roles := uu2\<rparr>)) \<and> pref (s\<lparr>roles := uu1\<rparr>) = pref (s1\<lparr>roles := uu2\<rparr>) \<and> voronkov (s\<lparr>roles := uu1\<rparr>) = voronkov (s1\<lparr>roles := uu2\<rparr>) \<and> news (s\<lparr>roles := uu1\<rparr>) = news (s1\<lparr>roles := uu2\<rparr>) \<and> phase (s\<lparr>roles := uu1\<rparr>) = phase (s1\<lparr>roles := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>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; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>paperIDs := uu1\<rparr>) = confIDs (s1\<lparr>paperIDs := uu2\<rparr>) \<and> conf (s\<lparr>paperIDs := uu1\<rparr>) = conf (s1\<lparr>paperIDs := uu2\<rparr>) \<and> userIDs (s\<lparr>paperIDs := uu1\<rparr>) = userIDs (s1\<lparr>paperIDs := uu2\<rparr>) \<and> pass (s\<lparr>paperIDs := uu1\<rparr>) = pass (s1\<lparr>paperIDs := uu2\<rparr>) \<and> user (s\<lparr>paperIDs := uu1\<rparr>) = user (s1\<lparr>paperIDs := uu2\<rparr>) \<and> roles (s\<lparr>paperIDs := uu1\<rparr>) = roles (s1\<lparr>paperIDs := uu2\<rparr>) \<and> paperIDs (s\<lparr>paperIDs := uu1\<rparr>) = paperIDs (s1\<lparr>paperIDs := uu2\<rparr>) \<and> eeqExcPID (paper (s\<lparr>paperIDs := uu1\<rparr>)) (paper (s1\<lparr>paperIDs := uu2\<rparr>)) \<and> pref (s\<lparr>paperIDs := uu1\<rparr>) = pref (s1\<lparr>paperIDs := uu2\<rparr>) \<and> voronkov (s\<lparr>paperIDs := uu1\<rparr>) = voronkov (s1\<lparr>paperIDs := uu2\<rparr>) \<and> news (s\<lparr>paperIDs := uu1\<rparr>) = news (s1\<lparr>paperIDs := uu2\<rparr>) \<and> phase (s\<lparr>paperIDs := uu1\<rparr>) = phase (s1\<lparr>paperIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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; eeqExcPID uu1 uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>paper := uu1\<rparr>) = confIDs (s1\<lparr>paper := uu2\<rparr>) \<and> conf (s\<lparr>paper := uu1\<rparr>) = conf (s1\<lparr>paper := uu2\<rparr>) \<and> userIDs (s\<lparr>paper := uu1\<rparr>) = userIDs (s1\<lparr>paper := uu2\<rparr>) \<and> pass (s\<lparr>paper := uu1\<rparr>) = pass (s1\<lparr>paper := uu2\<rparr>) \<and> user (s\<lparr>paper := uu1\<rparr>) = user (s1\<lparr>paper := uu2\<rparr>) \<and> roles (s\<lparr>paper := uu1\<rparr>) = roles (s1\<lparr>paper := uu2\<rparr>) \<and> paperIDs (s\<lparr>paper := uu1\<rparr>) = paperIDs (s1\<lparr>paper := uu2\<rparr>) \<and> eeqExcPID (paper (s\<lparr>paper := uu1\<rparr>)) (paper (s1\<lparr>paper := uu2\<rparr>)) \<and> pref (s\<lparr>paper := uu1\<rparr>) = pref (s1\<lparr>paper := uu2\<rparr>) \<and> voronkov (s\<lparr>paper := uu1\<rparr>) = voronkov (s1\<lparr>paper := uu2\<rparr>) \<and> news (s\<lparr>paper := uu1\<rparr>) = news (s1\<lparr>paper := uu2\<rparr>) \<and> phase (s\<lparr>paper := uu1\<rparr>) = phase (s1\<lparr>paper := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>pref := uu1\<rparr>) = confIDs (s1\<lparr>pref := uu2\<rparr>) \<and> conf (s\<lparr>pref := uu1\<rparr>) = conf (s1\<lparr>pref := uu2\<rparr>) \<and> userIDs (s\<lparr>pref := uu1\<rparr>) = userIDs (s1\<lparr>pref := uu2\<rparr>) \<and> pass (s\<lparr>pref := uu1\<rparr>) = pass (s1\<lparr>pref := uu2\<rparr>) \<and> user (s\<lparr>pref := uu1\<rparr>) = user (s1\<lparr>pref := uu2\<rparr>) \<and> roles (s\<lparr>pref := uu1\<rparr>) = roles (s1\<lparr>pref := uu2\<rparr>) \<and> paperIDs (s\<lparr>pref := uu1\<rparr>) = paperIDs (s1\<lparr>pref := uu2\<rparr>) \<and> eeqExcPID (paper (s\<lparr>pref := uu1\<rparr>)) (paper (s1\<lparr>pref := uu2\<rparr>)) \<and> pref (s\<lparr>pref := uu1\<rparr>) = pref (s1\<lparr>pref := uu2\<rparr>) \<and> voronkov (s\<lparr>pref := uu1\<rparr>) = voronkov (s1\<lparr>pref := uu2\<rparr>) \<and> news (s\<lparr>pref := uu1\<rparr>) = news (s1\<lparr>pref := uu2\<rparr>) \<and> phase (s\<lparr>pref := uu1\<rparr>) = phase (s1\<lparr>pref := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>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; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>voronkov := uu1\<rparr>) = confIDs (s1\<lparr>voronkov := uu2\<rparr>) \<and> conf (s\<lparr>voronkov := uu1\<rparr>) = conf (s1\<lparr>voronkov := uu2\<rparr>) \<and> userIDs (s\<lparr>voronkov := uu1\<rparr>) = userIDs (s1\<lparr>voronkov := uu2\<rparr>) \<and> pass (s\<lparr>voronkov := uu1\<rparr>) = pass (s1\<lparr>voronkov := uu2\<rparr>) \<and> user (s\<lparr>voronkov := uu1\<rparr>) = user (s1\<lparr>voronkov := uu2\<rparr>) \<and> roles (s\<lparr>voronkov := uu1\<rparr>) = roles (s1\<lparr>voronkov := uu2\<rparr>) \<and> paperIDs (s\<lparr>voronkov := uu1\<rparr>) = paperIDs (s1\<lparr>voronkov := uu2\<rparr>) \<and> eeqExcPID (paper (s\<lparr>voronkov := uu1\<rparr>)) (paper (s1\<lparr>voronkov := uu2\<rparr>)) \<and> pref (s\<lparr>voronkov := uu1\<rparr>) = pref (s1\<lparr>voronkov := uu2\<rparr>) \<and> voronkov (s\<lparr>voronkov := uu1\<rparr>) = voronkov (s1\<lparr>voronkov := uu2\<rparr>) \<and> news (s\<lparr>voronkov := uu1\<rparr>) = news (s1\<lparr>voronkov := uu2\<rparr>) \<and> phase (s\<lparr>voronkov := uu1\<rparr>) = phase (s1\<lparr>voronkov := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>news := uu1\<rparr>) = confIDs (s1\<lparr>news := uu2\<rparr>) \<and> conf (s\<lparr>news := uu1\<rparr>) = conf (s1\<lparr>news := uu2\<rparr>) \<and> userIDs (s\<lparr>news := uu1\<rparr>) = userIDs (s1\<lparr>news := uu2\<rparr>) \<and> pass (s\<lparr>news := uu1\<rparr>) = pass (s1\<lparr>news := uu2\<rparr>) \<and> user (s\<lparr>news := uu1\<rparr>) = user (s1\<lparr>news := uu2\<rparr>) \<and> roles (s\<lparr>news := uu1\<rparr>) = roles (s1\<lparr>news := uu2\<rparr>) \<and> paperIDs (s\<lparr>news := uu1\<rparr>) = paperIDs (s1\<lparr>news := uu2\<rparr>) \<and> eeqExcPID (paper (s\<lparr>news := uu1\<rparr>)) (paper (s1\<lparr>news := uu2\<rparr>)) \<and> pref (s\<lparr>news := uu1\<rparr>) = pref (s1\<lparr>news := uu2\<rparr>) \<and> voronkov (s\<lparr>news := uu1\<rparr>) = voronkov (s1\<lparr>news := uu2\<rparr>) \<and> news (s\<lparr>news := uu1\<rparr>) = news (s1\<lparr>news := uu2\<rparr>) \<and> phase (s\<lparr>news := uu1\<rparr>) = phase (s1\<lparr>news := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>phase := uu1\<rparr>) = confIDs (s1\<lparr>phase := uu2\<rparr>) \<and> conf (s\<lparr>phase := uu1\<rparr>) = conf (s1\<lparr>phase := uu2\<rparr>) \<and> userIDs (s\<lparr>phase := uu1\<rparr>) = userIDs (s1\<lparr>phase := uu2\<rparr>) \<and> pass (s\<lparr>phase := uu1\<rparr>) = pass (s1\<lparr>phase := uu2\<rparr>) \<and> user (s\<lparr>phase := uu1\<rparr>) = user (s1\<lparr>phase := uu2\<rparr>) \<and> roles (s\<lparr>phase := uu1\<rparr>) = roles (s1\<lparr>phase := uu2\<rparr>) \<and> paperIDs (s\<lparr>phase := uu1\<rparr>) = paperIDs (s1\<lparr>phase := uu2\<rparr>) \<and> eeqExcPID (paper (s\<lparr>phase := uu1\<rparr>)) (paper (s1\<lparr>phase := uu2\<rparr>)) \<and> pref (s\<lparr>phase := uu1\<rparr>) = pref (s1\<lparr>phase := uu2\<rparr>) \<and> voronkov (s\<lparr>phase := uu1\<rparr>) = voronkov (s1\<lparr>phase := uu2\<rparr>) \<and> news (s\<lparr>phase := uu1\<rparr>) = news (s1\<lparr>phase := uu2\<rparr>) \<and> phase (s\<lparr>phase := uu1\<rparr>) = phase (s1\<lparr>phase := uu2\<rparr>))
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcPID_Paper:
assumes s's1': "eqExcPID s s1"
and "paper s pid = Paper title abstract content reviews dis decs"
and "paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1"
shows "title = title1 \<and> abstract = abstract1 \<and> content = content1 \<and> reviews = reviews1 \<and> dis = dis1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. title = title1 \<and> abstract = abstract1 \<and> content = content1 \<and> reviews = reviews1 \<and> dis = dis1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqExcPID s s1
paper s pid = Paper title abstract content reviews dis decs
paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1

goal (1 subgoal):
 1. title = title1 \<and> abstract = abstract1 \<and> content = content1 \<and> reviews = reviews1 \<and> dis = dis1
[PROOF STEP]
unfolding eqExcPID_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 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1
paper s pid = Paper title abstract content reviews dis decs
paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1

goal (1 subgoal):
 1. title = title1 \<and> abstract = abstract1 \<and> content = content1 \<and> reviews = reviews1 \<and> dis = dis1
[PROOF STEP]
apply (auto simp: eqExcD eeqExcPID_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>paper s pid = Paper title abstract content reviews dis decs; paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1; confIDs s = confIDs s1; conf s = conf s1; userIDs s = userIDs s1; pass s = pass s1; user s = user s1; roles s = roles s1; paperIDs s = paperIDs s1; \<forall>pid. (pid = PID \<longrightarrow> reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and> contentPaper (paper s PID) = contentPaper (paper s1 PID) \<and> abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \<and> titlePaper (paper s PID) = titlePaper (paper s1 PID) \<and> disPaper (paper s PID) = disPaper (paper s1 PID)) \<and> (pid = PID \<or> paper s pid = paper s1 pid); pref s = pref s1; voronkov s = voronkov s1; news s = news s1; phase s = phase s1\<rbrakk> \<Longrightarrow> title = title1
 2. \<lbrakk>paper s pid = Paper title abstract content reviews dis decs; paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1; confIDs s = confIDs s1; conf s = conf s1; userIDs s = userIDs s1; pass s = pass s1; user s = user s1; roles s = roles s1; paperIDs s = paperIDs s1; \<forall>pid. (pid = PID \<longrightarrow> reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and> contentPaper (paper s PID) = contentPaper (paper s1 PID) \<and> abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \<and> titlePaper (paper s PID) = titlePaper (paper s1 PID) \<and> disPaper (paper s PID) = disPaper (paper s1 PID)) \<and> (pid = PID \<or> paper s pid = paper s1 pid); pref s = pref s1; voronkov s = voronkov s1; news s = news s1; phase s = phase s1\<rbrakk> \<Longrightarrow> abstract = abstract1
 3. \<lbrakk>paper s pid = Paper title abstract content reviews dis decs; paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1; confIDs s = confIDs s1; conf s = conf s1; userIDs s = userIDs s1; pass s = pass s1; user s = user s1; roles s = roles s1; paperIDs s = paperIDs s1; \<forall>pid. (pid = PID \<longrightarrow> reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and> contentPaper (paper s PID) = contentPaper (paper s1 PID) \<and> abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \<and> titlePaper (paper s PID) = titlePaper (paper s1 PID) \<and> disPaper (paper s PID) = disPaper (paper s1 PID)) \<and> (pid = PID \<or> paper s pid = paper s1 pid); pref s = pref s1; voronkov s = voronkov s1; news s = news s1; phase s = phase s1\<rbrakk> \<Longrightarrow> content = content1
 4. \<lbrakk>paper s pid = Paper title abstract content reviews dis decs; paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1; confIDs s = confIDs s1; conf s = conf s1; userIDs s = userIDs s1; pass s = pass s1; user s = user s1; roles s = roles s1; paperIDs s = paperIDs s1; \<forall>pid. (pid = PID \<longrightarrow> reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and> contentPaper (paper s PID) = contentPaper (paper s1 PID) \<and> abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \<and> titlePaper (paper s PID) = titlePaper (paper s1 PID) \<and> disPaper (paper s PID) = disPaper (paper s1 PID)) \<and> (pid = PID \<or> paper s pid = paper s1 pid); pref s = pref s1; voronkov s = voronkov s1; news s = news s1; phase s = phase s1\<rbrakk> \<Longrightarrow> reviews = reviews1
 5. \<lbrakk>paper s pid = Paper title abstract content reviews dis decs; paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1; confIDs s = confIDs s1; conf s = conf s1; userIDs s = userIDs s1; pass s = pass s1; user s = user s1; roles s = roles s1; paperIDs s = paperIDs s1; \<forall>pid. (pid = PID \<longrightarrow> reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and> contentPaper (paper s PID) = contentPaper (paper s1 PID) \<and> abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \<and> titlePaper (paper s PID) = titlePaper (paper s1 PID) \<and> disPaper (paper s PID) = disPaper (paper s1 PID)) \<and> (pid = PID \<or> paper s pid = paper s1 pid); pref s = pref s1; voronkov s = voronkov s1; news s = news s1; phase s = phase s1\<rbrakk> \<Longrightarrow> dis = dis1
[PROOF STEP]
by (metis titlePaper.simps abstractPaper.simps contentPaper.simps reviewsPaper.simps disPaper.simps
          )+


[STATEMENT]
lemma eqExcD2:
"eqExcD2 pap pap1 =
 (titlePaper pap = titlePaper pap1 \<and> abstractPaper pap = abstractPaper pap1 \<and>
  contentPaper pap = contentPaper pap1 \<and>
  reviewsPaper pap = reviewsPaper pap1 \<and> disPaper pap = disPaper pap1 \<and>
  hd (decsPaper pap) = hd (decsPaper pap1)
 )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcD2 pap pap1 = (titlePaper pap = titlePaper pap1 \<and> abstractPaper pap = abstractPaper pap1 \<and> contentPaper pap = contentPaper pap1 \<and> reviewsPaper pap = reviewsPaper pap1 \<and> disPaper pap = disPaper pap1 \<and> hd (decsPaper pap) = hd (decsPaper pap1))
[PROOF STEP]
by(cases pap, cases pap1, auto)


[STATEMENT]
lemma eqExcD2_eq[simp,intro!]: "eqExcD2 pap pap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcD2 pap pap
[PROOF STEP]
by(cases pap) auto


[STATEMENT]
lemma eqExcD2_sym:
assumes "eqExcD2 pap pap1"
shows "eqExcD2 pap1 pap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcD2 pap1 pap
[PROOF STEP]
apply(cases pap, cases pap1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x1a x2a x3a x4a x5a x6a. \<lbrakk>pap = Paper x1 x2 x3 x4 x5 x6; pap1 = Paper x1a x2a x3a x4a x5a x6a\<rbrakk> \<Longrightarrow> eqExcD2 pap1 pap
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqExcD2 pap pap1

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x1a x2a x3a x4a x5a x6a. \<lbrakk>pap = Paper x1 x2 x3 x4 x5 x6; pap1 = Paper x1a x2a x3a x4a x5a x6a\<rbrakk> \<Longrightarrow> eqExcD2 pap1 pap
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcD2_trans:
assumes "eqExcD2 pap pap1" and "eqExcD2 pap1 pap2"
shows "eqExcD2 pap pap2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcD2 pap pap2
[PROOF STEP]
apply(cases pap, cases pap1, cases pap2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x1a x2a x3a x4a x5a x6a x1b x2b x3b x4b x5b x6b. \<lbrakk>pap = Paper x1 x2 x3 x4 x5 x6; pap1 = Paper x1a x2a x3a x4a x5a x6a; pap2 = Paper x1b x2b x3b x4b x5b x6b\<rbrakk> \<Longrightarrow> eqExcD2 pap pap2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqExcD2 pap pap1
eqExcD2 pap1 pap2

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x1a x2a x3a x4a x5a x6a x1b x2b x3b x4b x5b x6b. \<lbrakk>pap = Paper x1 x2 x3 x4 x5 x6; pap1 = Paper x1a x2a x3a x4a x5a x6a; pap2 = Paper x1b x2b x3b x4b x5b x6b\<rbrakk> \<Longrightarrow> eqExcD2 pap pap2
[PROOF STEP]
by auto


[STATEMENT]
lemma eeqExcPID2_eeq[simp,intro!]: "eeqExcPID2 s s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eeqExcPID2 s s
[PROOF STEP]
unfolding eeqExcPID2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>pid. if pid = PID then eqExcD2 (s pid) (s pid) else s pid = s pid
[PROOF STEP]
by auto


[STATEMENT]
lemma eeqExcPID2_sym:
assumes "eeqExcPID2 s s1" shows "eeqExcPID2 s1 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eeqExcPID2 s1 s
[PROOF STEP]
using assms eqExcD2_sym
[PROOF STATE]
proof (prove)
using this:
eeqExcPID2 s s1
eqExcD2 ?pap ?pap1.0 \<Longrightarrow> eqExcD2 ?pap1.0 ?pap

goal (1 subgoal):
 1. eeqExcPID2 s1 s
[PROOF STEP]
unfolding eeqExcPID2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>pid. if pid = PID then eqExcD2 (s pid) (s1 pid) else s pid = s1 pid
eqExcD2 ?pap ?pap1.0 \<Longrightarrow> eqExcD2 ?pap1.0 ?pap

goal (1 subgoal):
 1. \<forall>pid. if pid = PID then eqExcD2 (s1 pid) (s pid) else s1 pid = s pid
[PROOF STEP]
by auto


[STATEMENT]
lemma eeqExcPID2_trans:
assumes "eeqExcPID2 s s1" and "eeqExcPID2 s1 s2" shows "eeqExcPID2 s s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eeqExcPID2 s s2
[PROOF STEP]
using assms eqExcD2_trans
[PROOF STATE]
proof (prove)
using this:
eeqExcPID2 s s1
eeqExcPID2 s1 s2
\<lbrakk>eqExcD2 ?pap ?pap1.0; eqExcD2 ?pap1.0 ?pap2.0\<rbrakk> \<Longrightarrow> eqExcD2 ?pap ?pap2.0

goal (1 subgoal):
 1. eeqExcPID2 s s2
[PROOF STEP]
unfolding eeqExcPID2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>pid. if pid = PID then eqExcD2 (s pid) (s1 pid) else s pid = s1 pid
\<forall>pid. if pid = PID then eqExcD2 (s1 pid) (s2 pid) else s1 pid = s2 pid
\<lbrakk>eqExcD2 ?pap ?pap1.0; eqExcD2 ?pap1.0 ?pap2.0\<rbrakk> \<Longrightarrow> eqExcD2 ?pap ?pap2.0

goal (1 subgoal):
 1. \<forall>pid. if pid = PID then eqExcD2 (s pid) (s2 pid) else s pid = s2 pid
[PROOF STEP]
by simp blast


[STATEMENT]
lemma eeqExcPID2_imp:
"eeqExcPID2 paps paps1 \<Longrightarrow> eqExcD2 (paps PID) (paps1 PID)"
"\<lbrakk>eeqExcPID2 paps paps1; pid \<noteq> PID\<rbrakk> \<Longrightarrow> paps pid = paps1 pid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (eeqExcPID2 paps paps1 \<Longrightarrow> eqExcD2 (paps PID) (paps1 PID)) &&& (\<lbrakk>eeqExcPID2 paps paps1; pid \<noteq> PID\<rbrakk> \<Longrightarrow> paps pid = paps1 pid)
[PROOF STEP]
unfolding eeqExcPID2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>pid. if pid = PID then eqExcD2 (paps pid) (paps1 pid) else paps pid = paps1 pid \<Longrightarrow> eqExcD2 (paps PID) (paps1 PID)) &&& (\<lbrakk>\<forall>pid. if pid = PID then eqExcD2 (paps pid) (paps1 pid) else paps pid = paps1 pid; pid \<noteq> PID\<rbrakk> \<Longrightarrow> paps pid = paps1 pid)
[PROOF STEP]
by auto


[STATEMENT]
lemma eeqExcPID2_cong:
assumes "eeqExcPID2 paps paps1"
and "pid = PID \<Longrightarrow> eqExcD2 uu uu1"
and "pid \<noteq> PID \<Longrightarrow> uu = uu1"
shows "eeqExcPID2 (paps (pid := uu)) (paps1(pid := uu1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eeqExcPID2 (paps(pid := uu)) (paps1(pid := uu1))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eeqExcPID2 paps paps1
pid = PID \<Longrightarrow> eqExcD2 uu uu1
pid \<noteq> PID \<Longrightarrow> uu = uu1

goal (1 subgoal):
 1. eeqExcPID2 (paps(pid := uu)) (paps1(pid := uu1))
[PROOF STEP]
unfolding eeqExcPID2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>pid. if pid = PID then eqExcD2 (paps pid) (paps1 pid) else paps pid = paps1 pid
pid = PID \<Longrightarrow> eqExcD2 uu uu1
pid \<noteq> PID \<Longrightarrow> uu = uu1

goal (1 subgoal):
 1. \<forall>pida. if pida = PID then eqExcD2 ((paps(pid := uu)) pida) ((paps1(pid := uu1)) pida) else (paps(pid := uu)) pida = (paps1(pid := uu1)) pida
[PROOF STEP]
by auto


[STATEMENT]
lemma eeqExcPID2_RDD:
"eeqExcPID2 paps paps1 \<Longrightarrow>
 titlePaper (paps PID) = titlePaper (paps1 PID) \<and>
 abstractPaper (paps PID) = abstractPaper (paps1 PID) \<and>
 contentPaper (paps PID) = contentPaper (paps1 PID) \<and>
 reviewsPaper (paps PID) = reviewsPaper (paps1 PID) \<and>
 disPaper (paps PID) = disPaper (paps1 PID) \<and>
 hd (decsPaper (paps PID)) = hd (decsPaper (paps PID))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eeqExcPID2 paps paps1 \<Longrightarrow> titlePaper (paps PID) = titlePaper (paps1 PID) \<and> abstractPaper (paps PID) = abstractPaper (paps1 PID) \<and> contentPaper (paps PID) = contentPaper (paps1 PID) \<and> reviewsPaper (paps PID) = reviewsPaper (paps1 PID) \<and> disPaper (paps PID) = disPaper (paps1 PID) \<and> hd (decsPaper (paps PID)) = hd (decsPaper (paps PID))
[PROOF STEP]
using eeqExcPID2_def
[PROOF STATE]
proof (prove)
using this:
eeqExcPID2 ?paps ?paps1.0 \<equiv> \<forall>pid. if pid = PID then eqExcD2 (?paps pid) (?paps1.0 pid) else ?paps pid = ?paps1.0 pid

goal (1 subgoal):
 1. eeqExcPID2 paps paps1 \<Longrightarrow> titlePaper (paps PID) = titlePaper (paps1 PID) \<and> abstractPaper (paps PID) = abstractPaper (paps1 PID) \<and> contentPaper (paps PID) = contentPaper (paps1 PID) \<and> reviewsPaper (paps PID) = reviewsPaper (paps1 PID) \<and> disPaper (paps PID) = disPaper (paps1 PID) \<and> hd (decsPaper (paps PID)) = hd (decsPaper (paps PID))
[PROOF STEP]
unfolding eqExcD2
[PROOF STATE]
proof (prove)
using this:
eeqExcPID2 ?paps ?paps1.0 \<equiv> \<forall>pid. if pid = PID then titlePaper (?paps pid) = titlePaper (?paps1.0 pid) \<and> abstractPaper (?paps pid) = abstractPaper (?paps1.0 pid) \<and> contentPaper (?paps pid) = contentPaper (?paps1.0 pid) \<and> reviewsPaper (?paps pid) = reviewsPaper (?paps1.0 pid) \<and> disPaper (?paps pid) = disPaper (?paps1.0 pid) \<and> hd (decsPaper (?paps pid)) = hd (decsPaper (?paps1.0 pid)) else ?paps pid = ?paps1.0 pid

goal (1 subgoal):
 1. eeqExcPID2 paps paps1 \<Longrightarrow> titlePaper (paps PID) = titlePaper (paps1 PID) \<and> abstractPaper (paps PID) = abstractPaper (paps1 PID) \<and> contentPaper (paps PID) = contentPaper (paps1 PID) \<and> reviewsPaper (paps PID) = reviewsPaper (paps1 PID) \<and> disPaper (paps PID) = disPaper (paps1 PID) \<and> hd (decsPaper (paps PID)) = hd (decsPaper (paps PID))
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcPID2_eq[simp,intro!]: "eqExcPID2 s s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID2 s s
[PROOF STEP]
unfolding eqExcPID2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. confIDs s = confIDs s \<and> conf s = conf s \<and> userIDs s = userIDs s \<and> pass s = pass s \<and> user s = user s \<and> roles s = roles s \<and> paperIDs s = paperIDs s \<and> eeqExcPID2 (paper s) (paper s) \<and> pref s = pref s \<and> voronkov s = voronkov s \<and> news s = news s \<and> phase s = phase s
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcPID2_sym:
assumes "eqExcPID2 s s1" shows "eqExcPID2 s1 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID2 s1 s
[PROOF STEP]
using assms eeqExcPID2_sym
[PROOF STATE]
proof (prove)
using this:
eqExcPID2 s s1
eeqExcPID2 ?s ?s1.0 \<Longrightarrow> eeqExcPID2 ?s1.0 ?s

goal (1 subgoal):
 1. eqExcPID2 s1 s
[PROOF STEP]
unfolding eqExcPID2_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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1
eeqExcPID2 ?s ?s1.0 \<Longrightarrow> eeqExcPID2 ?s1.0 ?s

goal (1 subgoal):
 1. confIDs s1 = confIDs s \<and> conf s1 = conf s \<and> userIDs s1 = userIDs s \<and> pass s1 = pass s \<and> user s1 = user s \<and> roles s1 = roles s \<and> paperIDs s1 = paperIDs s \<and> eeqExcPID2 (paper s1) (paper s) \<and> pref s1 = pref s \<and> voronkov s1 = voronkov s \<and> news s1 = news s \<and> phase s1 = phase s
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcPID2_trans:
assumes "eqExcPID2 s s1" and "eqExcPID2 s1 s2" shows "eqExcPID2 s s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID2 s s2
[PROOF STEP]
using assms eeqExcPID2_trans
[PROOF STATE]
proof (prove)
using this:
eqExcPID2 s s1
eqExcPID2 s1 s2
\<lbrakk>eeqExcPID2 ?s ?s1.0; eeqExcPID2 ?s1.0 ?s2.0\<rbrakk> \<Longrightarrow> eeqExcPID2 ?s ?s2.0

goal (1 subgoal):
 1. eqExcPID2 s s2
[PROOF STEP]
unfolding eqExcPID2_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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1
confIDs s1 = confIDs s2 \<and> conf s1 = conf s2 \<and> userIDs s1 = userIDs s2 \<and> pass s1 = pass s2 \<and> user s1 = user s2 \<and> roles s1 = roles s2 \<and> paperIDs s1 = paperIDs s2 \<and> eeqExcPID2 (paper s1) (paper s2) \<and> pref s1 = pref s2 \<and> voronkov s1 = voronkov s2 \<and> news s1 = news s2 \<and> phase s1 = phase s2
\<lbrakk>eeqExcPID2 ?s ?s1.0; eeqExcPID2 ?s1.0 ?s2.0\<rbrakk> \<Longrightarrow> eeqExcPID2 ?s ?s2.0

goal (1 subgoal):
 1. confIDs s = confIDs s2 \<and> conf s = conf s2 \<and> userIDs s = userIDs s2 \<and> pass s = pass s2 \<and> user s = user s2 \<and> roles s = roles s2 \<and> paperIDs s = paperIDs s2 \<and> eeqExcPID2 (paper s) (paper s2) \<and> pref s = pref s2 \<and> voronkov s = voronkov s2 \<and> news s = news s2 \<and> phase s = phase s2
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcPID2_imp:
"eqExcPID2 s s1 \<Longrightarrow>
 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>
 eeqExcPID2 (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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID2 s s1 \<Longrightarrow> 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> eeqExcPID2 (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
[PROOF STEP]
unfolding eqExcPID2_def getAllPaperIDs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1 \<Longrightarrow> 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> eeqExcPID2 (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> cmap (paperIDs s) (confIDs s) = cmap (paperIDs s1) (confIDs 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
[PROOF STEP]
unfolding isRev_def getReviewIndex_def getRevRole_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1 \<Longrightarrow> 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> eeqExcPID2 (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> cmap (paperIDs s) (confIDs s) = cmap (paperIDs s1) (confIDs s1) \<and> list_ex (isRevRoleFor pid) (roles s cid uid) = list_ex (isRevRoleFor pid) (roles s1 cid uid) \<and> (case find (isRevRoleFor pid) (roles s cid uid) of Some (Rev papID' n) \<Rightarrow> n) = (case find (isRevRoleFor pid) (roles s1 cid uid) of Some (Rev papID' n) \<Rightarrow> n) \<and> find (isRevRoleFor pid) (roles s cid uid) = find (isRevRoleFor pid) (roles s1 cid uid)
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcPID2_imp1:
"eqExcPID2 s s1 \<Longrightarrow> eqExcD2 (paper s pid) (paper s1 pid)"
"eqExcPID2 s s1 \<Longrightarrow> pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow>
    paper s pid = paper s1 pid \<and>
    getNthReview s pid n = getNthReview s1 pid n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (eqExcPID2 s s1 \<Longrightarrow> eqExcD2 (paper s pid) (paper s1 pid)) &&& (\<lbrakk>eqExcPID2 s s1; pid \<noteq> PID \<or> PID \<noteq> pid\<rbrakk> \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n)
[PROOF STEP]
unfolding eqExcPID2_def getNthReview_def eeqExcPID2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (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 eqExcD2 (paper s pid) (paper s1 pid) 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 \<Longrightarrow> eqExcD2 (paper s pid) (paper s1 pid)) &&& (\<lbrakk>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 eqExcD2 (paper s pid) (paper s1 pid) 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; pid \<noteq> PID \<or> PID \<noteq> pid\<rbrakk> \<Longrightarrow> paper s pid = paper s1 pid \<and> reviewsPaper (paper s pid) ! n = reviewsPaper (paper s1 pid) ! n)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confIDs s = confIDs s1; conf s = conf s1; userIDs s = userIDs s1; pass s = pass s1; user s = user s1; roles s = roles s1; paperIDs s = paperIDs s1; \<forall>pid. (pid = PID \<longrightarrow> eqExcD2 (paper s PID) (paper s1 PID)) \<and> (pid = PID \<or> paper s pid = paper s1 pid); pref s = pref s1; voronkov s = voronkov s1; news s = news s1; phase s = phase s1\<rbrakk> \<Longrightarrow> eqExcD2 (paper s pid) (paper s1 pid)
[PROOF STEP]
by (metis eqExcD2_eq)


[STATEMENT]
lemma eqExcPID2_imp2:
assumes "eqExcPID2 s s1" and "pid \<noteq> PID \<or> PID \<noteq> pid"
shows "getReviewersReviews s cid pid = getReviewersReviews s1 cid pid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getReviewersReviews s cid pid = getReviewersReviews s1 cid pid
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. getReviewersReviews s cid pid = getReviewersReviews s1 cid pid
[PROOF STEP]
have
  "(\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) =
   (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uID. (if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqExcPID2 s s1
pid \<noteq> PID \<or> PID \<noteq> pid

goal (1 subgoal):
 1. \<And>uID. (if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])
[PROOF STEP]
by (auto simp: eqExcPID2_imp eqExcPID2_imp1)
[PROOF STATE]
proof (state)
this:
(\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])

goal (1 subgoal):
 1. getReviewersReviews s cid pid = getReviewersReviews s1 cid pid
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])

goal (1 subgoal):
 1. getReviewersReviews s cid pid = getReviewersReviews s1 cid pid
[PROOF STEP]
unfolding getReviewersReviews_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])

goal (1 subgoal):
 1. cmap (\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) (userIDs s) = cmap (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else []) (userIDs s1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) = (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])
eqExcPID2 s s1
pid \<noteq> PID \<or> PID \<noteq> pid

goal (1 subgoal):
 1. cmap (\<lambda>uID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) (userIDs s) = cmap (\<lambda>uID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else []) (userIDs s1)
[PROOF STEP]
by (simp add: eqExcPID2_imp)
[PROOF STATE]
proof (state)
this:
getReviewersReviews s cid pid = getReviewersReviews s1 cid pid

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqExcPID2_RDD:
"eqExcPID2 s s1 \<Longrightarrow>
 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>
 reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and>
 disPaper (paper s PID) = disPaper (paper s1 PID)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID2 s s1 \<Longrightarrow> 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> reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and> disPaper (paper s PID) = disPaper (paper s1 PID)
[PROOF STEP]
using eqExcPID2_imp eeqExcPID2_RDD
[PROOF STATE]
proof (prove)
using this:
eqExcPID2 ?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> eeqExcPID2 (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
eeqExcPID2 ?paps ?paps1.0 \<Longrightarrow> titlePaper (?paps PID) = titlePaper (?paps1.0 PID) \<and> abstractPaper (?paps PID) = abstractPaper (?paps1.0 PID) \<and> contentPaper (?paps PID) = contentPaper (?paps1.0 PID) \<and> reviewsPaper (?paps PID) = reviewsPaper (?paps1.0 PID) \<and> disPaper (?paps PID) = disPaper (?paps1.0 PID) \<and> hd (decsPaper (?paps PID)) = hd (decsPaper (?paps PID))

goal (1 subgoal):
 1. eqExcPID2 s s1 \<Longrightarrow> 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> reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and> disPaper (paper s PID) = disPaper (paper s1 PID)
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcPID2_cong[simp, intro]:
"\<And> uu1 uu2. eqExcPID2 s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID2 (s \<lparr>confIDs := uu1\<rparr>) (s1 \<lparr>confIDs := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID2 s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID2 (s \<lparr>conf := uu1\<rparr>) (s1 \<lparr>conf := uu2\<rparr>)"

"\<And> uu1 uu2. eqExcPID2 s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID2 (s \<lparr>userIDs := uu1\<rparr>) (s1 \<lparr>userIDs := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID2 s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID2 (s \<lparr>pass := uu1\<rparr>) (s1 \<lparr>pass := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID2 s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID2 (s \<lparr>user := uu1\<rparr>) (s1 \<lparr>user := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID2 s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID2 (s \<lparr>roles := uu1\<rparr>) (s1 \<lparr>roles := uu2\<rparr>)"

"\<And> uu1 uu2. eqExcPID2 s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID2 (s \<lparr>paperIDs := uu1\<rparr>) (s1 \<lparr>paperIDs := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID2 s s1 \<Longrightarrow> eeqExcPID2 uu1 uu2 \<Longrightarrow> eqExcPID2 (s \<lparr>paper := uu1\<rparr>) (s1 \<lparr>paper := uu2\<rparr>)"

"\<And> uu1 uu2. eqExcPID2 s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID2 (s \<lparr>pref := uu1\<rparr>) (s1 \<lparr>pref := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID2 s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID2 (s \<lparr>voronkov := uu1\<rparr>) (s1 \<lparr>voronkov := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID2 s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID2 (s \<lparr>news := uu1\<rparr>) (s1 \<lparr>news := uu2\<rparr>)"
"\<And> uu1 uu2. eqExcPID2 s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqExcPID2 (s \<lparr>phase := uu1\<rparr>) (s1 \<lparr>phase := uu2\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<And>uu1 uu2. \<lbrakk>eqExcPID2 s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID2 (s\<lparr>confIDs := uu1\<rparr>) (s1\<lparr>confIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID2 s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID2 (s\<lparr>conf := uu1\<rparr>) (s1\<lparr>conf := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID2 s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID2 (s\<lparr>userIDs := uu1\<rparr>) (s1\<lparr>userIDs := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID2 s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID2 (s\<lparr>pass := uu1\<rparr>) (s1\<lparr>pass := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID2 s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID2 (s\<lparr>user := uu1\<rparr>) (s1\<lparr>user := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID2 s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID2 (s\<lparr>roles := uu1\<rparr>) (s1\<lparr>roles := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>eqExcPID2 s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID2 (s\<lparr>paperIDs := uu1\<rparr>) (s1\<lparr>paperIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID2 s s1; eeqExcPID2 uu1 uu2\<rbrakk> \<Longrightarrow> eqExcPID2 (s\<lparr>paper := uu1\<rparr>) (s1\<lparr>paper := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID2 s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID2 (s\<lparr>pref := uu1\<rparr>) (s1\<lparr>pref := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID2 s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID2 (s\<lparr>voronkov := uu1\<rparr>) (s1\<lparr>voronkov := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID2 s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID2 (s\<lparr>news := uu1\<rparr>) (s1\<lparr>news := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqExcPID2 s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqExcPID2 (s\<lparr>phase := uu1\<rparr>) (s1\<lparr>phase := uu2\<rparr>))
[PROOF STEP]
unfolding eqExcPID2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<And>uu1 uu2. \<lbrakk>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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>confIDs := uu1\<rparr>) = confIDs (s1\<lparr>confIDs := uu2\<rparr>) \<and> conf (s\<lparr>confIDs := uu1\<rparr>) = conf (s1\<lparr>confIDs := uu2\<rparr>) \<and> userIDs (s\<lparr>confIDs := uu1\<rparr>) = userIDs (s1\<lparr>confIDs := uu2\<rparr>) \<and> pass (s\<lparr>confIDs := uu1\<rparr>) = pass (s1\<lparr>confIDs := uu2\<rparr>) \<and> user (s\<lparr>confIDs := uu1\<rparr>) = user (s1\<lparr>confIDs := uu2\<rparr>) \<and> roles (s\<lparr>confIDs := uu1\<rparr>) = roles (s1\<lparr>confIDs := uu2\<rparr>) \<and> paperIDs (s\<lparr>confIDs := uu1\<rparr>) = paperIDs (s1\<lparr>confIDs := uu2\<rparr>) \<and> eeqExcPID2 (paper (s\<lparr>confIDs := uu1\<rparr>)) (paper (s1\<lparr>confIDs := uu2\<rparr>)) \<and> pref (s\<lparr>confIDs := uu1\<rparr>) = pref (s1\<lparr>confIDs := uu2\<rparr>) \<and> voronkov (s\<lparr>confIDs := uu1\<rparr>) = voronkov (s1\<lparr>confIDs := uu2\<rparr>) \<and> news (s\<lparr>confIDs := uu1\<rparr>) = news (s1\<lparr>confIDs := uu2\<rparr>) \<and> phase (s\<lparr>confIDs := uu1\<rparr>) = phase (s1\<lparr>confIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>conf := uu1\<rparr>) = confIDs (s1\<lparr>conf := uu2\<rparr>) \<and> conf (s\<lparr>conf := uu1\<rparr>) = conf (s1\<lparr>conf := uu2\<rparr>) \<and> userIDs (s\<lparr>conf := uu1\<rparr>) = userIDs (s1\<lparr>conf := uu2\<rparr>) \<and> pass (s\<lparr>conf := uu1\<rparr>) = pass (s1\<lparr>conf := uu2\<rparr>) \<and> user (s\<lparr>conf := uu1\<rparr>) = user (s1\<lparr>conf := uu2\<rparr>) \<and> roles (s\<lparr>conf := uu1\<rparr>) = roles (s1\<lparr>conf := uu2\<rparr>) \<and> paperIDs (s\<lparr>conf := uu1\<rparr>) = paperIDs (s1\<lparr>conf := uu2\<rparr>) \<and> eeqExcPID2 (paper (s\<lparr>conf := uu1\<rparr>)) (paper (s1\<lparr>conf := uu2\<rparr>)) \<and> pref (s\<lparr>conf := uu1\<rparr>) = pref (s1\<lparr>conf := uu2\<rparr>) \<and> voronkov (s\<lparr>conf := uu1\<rparr>) = voronkov (s1\<lparr>conf := uu2\<rparr>) \<and> news (s\<lparr>conf := uu1\<rparr>) = news (s1\<lparr>conf := uu2\<rparr>) \<and> phase (s\<lparr>conf := uu1\<rparr>) = phase (s1\<lparr>conf := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>userIDs := uu1\<rparr>) = confIDs (s1\<lparr>userIDs := uu2\<rparr>) \<and> conf (s\<lparr>userIDs := uu1\<rparr>) = conf (s1\<lparr>userIDs := uu2\<rparr>) \<and> userIDs (s\<lparr>userIDs := uu1\<rparr>) = userIDs (s1\<lparr>userIDs := uu2\<rparr>) \<and> pass (s\<lparr>userIDs := uu1\<rparr>) = pass (s1\<lparr>userIDs := uu2\<rparr>) \<and> user (s\<lparr>userIDs := uu1\<rparr>) = user (s1\<lparr>userIDs := uu2\<rparr>) \<and> roles (s\<lparr>userIDs := uu1\<rparr>) = roles (s1\<lparr>userIDs := uu2\<rparr>) \<and> paperIDs (s\<lparr>userIDs := uu1\<rparr>) = paperIDs (s1\<lparr>userIDs := uu2\<rparr>) \<and> eeqExcPID2 (paper (s\<lparr>userIDs := uu1\<rparr>)) (paper (s1\<lparr>userIDs := uu2\<rparr>)) \<and> pref (s\<lparr>userIDs := uu1\<rparr>) = pref (s1\<lparr>userIDs := uu2\<rparr>) \<and> voronkov (s\<lparr>userIDs := uu1\<rparr>) = voronkov (s1\<lparr>userIDs := uu2\<rparr>) \<and> news (s\<lparr>userIDs := uu1\<rparr>) = news (s1\<lparr>userIDs := uu2\<rparr>) \<and> phase (s\<lparr>userIDs := uu1\<rparr>) = phase (s1\<lparr>userIDs := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>pass := uu1\<rparr>) = confIDs (s1\<lparr>pass := uu2\<rparr>) \<and> conf (s\<lparr>pass := uu1\<rparr>) = conf (s1\<lparr>pass := uu2\<rparr>) \<and> userIDs (s\<lparr>pass := uu1\<rparr>) = userIDs (s1\<lparr>pass := uu2\<rparr>) \<and> pass (s\<lparr>pass := uu1\<rparr>) = pass (s1\<lparr>pass := uu2\<rparr>) \<and> user (s\<lparr>pass := uu1\<rparr>) = user (s1\<lparr>pass := uu2\<rparr>) \<and> roles (s\<lparr>pass := uu1\<rparr>) = roles (s1\<lparr>pass := uu2\<rparr>) \<and> paperIDs (s\<lparr>pass := uu1\<rparr>) = paperIDs (s1\<lparr>pass := uu2\<rparr>) \<and> eeqExcPID2 (paper (s\<lparr>pass := uu1\<rparr>)) (paper (s1\<lparr>pass := uu2\<rparr>)) \<and> pref (s\<lparr>pass := uu1\<rparr>) = pref (s1\<lparr>pass := uu2\<rparr>) \<and> voronkov (s\<lparr>pass := uu1\<rparr>) = voronkov (s1\<lparr>pass := uu2\<rparr>) \<and> news (s\<lparr>pass := uu1\<rparr>) = news (s1\<lparr>pass := uu2\<rparr>) \<and> phase (s\<lparr>pass := uu1\<rparr>) = phase (s1\<lparr>pass := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>user := uu1\<rparr>) = confIDs (s1\<lparr>user := uu2\<rparr>) \<and> conf (s\<lparr>user := uu1\<rparr>) = conf (s1\<lparr>user := uu2\<rparr>) \<and> userIDs (s\<lparr>user := uu1\<rparr>) = userIDs (s1\<lparr>user := uu2\<rparr>) \<and> pass (s\<lparr>user := uu1\<rparr>) = pass (s1\<lparr>user := uu2\<rparr>) \<and> user (s\<lparr>user := uu1\<rparr>) = user (s1\<lparr>user := uu2\<rparr>) \<and> roles (s\<lparr>user := uu1\<rparr>) = roles (s1\<lparr>user := uu2\<rparr>) \<and> paperIDs (s\<lparr>user := uu1\<rparr>) = paperIDs (s1\<lparr>user := uu2\<rparr>) \<and> eeqExcPID2 (paper (s\<lparr>user := uu1\<rparr>)) (paper (s1\<lparr>user := uu2\<rparr>)) \<and> pref (s\<lparr>user := uu1\<rparr>) = pref (s1\<lparr>user := uu2\<rparr>) \<and> voronkov (s\<lparr>user := uu1\<rparr>) = voronkov (s1\<lparr>user := uu2\<rparr>) \<and> news (s\<lparr>user := uu1\<rparr>) = news (s1\<lparr>user := uu2\<rparr>) \<and> phase (s\<lparr>user := uu1\<rparr>) = phase (s1\<lparr>user := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>roles := uu1\<rparr>) = confIDs (s1\<lparr>roles := uu2\<rparr>) \<and> conf (s\<lparr>roles := uu1\<rparr>) = conf (s1\<lparr>roles := uu2\<rparr>) \<and> userIDs (s\<lparr>roles := uu1\<rparr>) = userIDs (s1\<lparr>roles := uu2\<rparr>) \<and> pass (s\<lparr>roles := uu1\<rparr>) = pass (s1\<lparr>roles := uu2\<rparr>) \<and> user (s\<lparr>roles := uu1\<rparr>) = user (s1\<lparr>roles := uu2\<rparr>) \<and> roles (s\<lparr>roles := uu1\<rparr>) = roles (s1\<lparr>roles := uu2\<rparr>) \<and> paperIDs (s\<lparr>roles := uu1\<rparr>) = paperIDs (s1\<lparr>roles := uu2\<rparr>) \<and> eeqExcPID2 (paper (s\<lparr>roles := uu1\<rparr>)) (paper (s1\<lparr>roles := uu2\<rparr>)) \<and> pref (s\<lparr>roles := uu1\<rparr>) = pref (s1\<lparr>roles := uu2\<rparr>) \<and> voronkov (s\<lparr>roles := uu1\<rparr>) = voronkov (s1\<lparr>roles := uu2\<rparr>) \<and> news (s\<lparr>roles := uu1\<rparr>) = news (s1\<lparr>roles := uu2\<rparr>) \<and> phase (s\<lparr>roles := uu1\<rparr>) = phase (s1\<lparr>roles := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>paperIDs := uu1\<rparr>) = confIDs (s1\<lparr>paperIDs := uu2\<rparr>) \<and> conf (s\<lparr>paperIDs := uu1\<rparr>) = conf (s1\<lparr>paperIDs := uu2\<rparr>) \<and> userIDs (s\<lparr>paperIDs := uu1\<rparr>) = userIDs (s1\<lparr>paperIDs := uu2\<rparr>) \<and> pass (s\<lparr>paperIDs := uu1\<rparr>) = pass (s1\<lparr>paperIDs := uu2\<rparr>) \<and> user (s\<lparr>paperIDs := uu1\<rparr>) = user (s1\<lparr>paperIDs := uu2\<rparr>) \<and> roles (s\<lparr>paperIDs := uu1\<rparr>) = roles (s1\<lparr>paperIDs := uu2\<rparr>) \<and> paperIDs (s\<lparr>paperIDs := uu1\<rparr>) = paperIDs (s1\<lparr>paperIDs := uu2\<rparr>) \<and> eeqExcPID2 (paper (s\<lparr>paperIDs := uu1\<rparr>)) (paper (s1\<lparr>paperIDs := uu2\<rparr>)) \<and> pref (s\<lparr>paperIDs := uu1\<rparr>) = pref (s1\<lparr>paperIDs := uu2\<rparr>) \<and> voronkov (s\<lparr>paperIDs := uu1\<rparr>) = voronkov (s1\<lparr>paperIDs := uu2\<rparr>) \<and> news (s\<lparr>paperIDs := uu1\<rparr>) = news (s1\<lparr>paperIDs := uu2\<rparr>) \<and> phase (s\<lparr>paperIDs := uu1\<rparr>) = phase (s1\<lparr>paperIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1; eeqExcPID2 uu1 uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>paper := uu1\<rparr>) = confIDs (s1\<lparr>paper := uu2\<rparr>) \<and> conf (s\<lparr>paper := uu1\<rparr>) = conf (s1\<lparr>paper := uu2\<rparr>) \<and> userIDs (s\<lparr>paper := uu1\<rparr>) = userIDs (s1\<lparr>paper := uu2\<rparr>) \<and> pass (s\<lparr>paper := uu1\<rparr>) = pass (s1\<lparr>paper := uu2\<rparr>) \<and> user (s\<lparr>paper := uu1\<rparr>) = user (s1\<lparr>paper := uu2\<rparr>) \<and> roles (s\<lparr>paper := uu1\<rparr>) = roles (s1\<lparr>paper := uu2\<rparr>) \<and> paperIDs (s\<lparr>paper := uu1\<rparr>) = paperIDs (s1\<lparr>paper := uu2\<rparr>) \<and> eeqExcPID2 (paper (s\<lparr>paper := uu1\<rparr>)) (paper (s1\<lparr>paper := uu2\<rparr>)) \<and> pref (s\<lparr>paper := uu1\<rparr>) = pref (s1\<lparr>paper := uu2\<rparr>) \<and> voronkov (s\<lparr>paper := uu1\<rparr>) = voronkov (s1\<lparr>paper := uu2\<rparr>) \<and> news (s\<lparr>paper := uu1\<rparr>) = news (s1\<lparr>paper := uu2\<rparr>) \<and> phase (s\<lparr>paper := uu1\<rparr>) = phase (s1\<lparr>paper := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>pref := uu1\<rparr>) = confIDs (s1\<lparr>pref := uu2\<rparr>) \<and> conf (s\<lparr>pref := uu1\<rparr>) = conf (s1\<lparr>pref := uu2\<rparr>) \<and> userIDs (s\<lparr>pref := uu1\<rparr>) = userIDs (s1\<lparr>pref := uu2\<rparr>) \<and> pass (s\<lparr>pref := uu1\<rparr>) = pass (s1\<lparr>pref := uu2\<rparr>) \<and> user (s\<lparr>pref := uu1\<rparr>) = user (s1\<lparr>pref := uu2\<rparr>) \<and> roles (s\<lparr>pref := uu1\<rparr>) = roles (s1\<lparr>pref := uu2\<rparr>) \<and> paperIDs (s\<lparr>pref := uu1\<rparr>) = paperIDs (s1\<lparr>pref := uu2\<rparr>) \<and> eeqExcPID2 (paper (s\<lparr>pref := uu1\<rparr>)) (paper (s1\<lparr>pref := uu2\<rparr>)) \<and> pref (s\<lparr>pref := uu1\<rparr>) = pref (s1\<lparr>pref := uu2\<rparr>) \<and> voronkov (s\<lparr>pref := uu1\<rparr>) = voronkov (s1\<lparr>pref := uu2\<rparr>) \<and> news (s\<lparr>pref := uu1\<rparr>) = news (s1\<lparr>pref := uu2\<rparr>) \<and> phase (s\<lparr>pref := uu1\<rparr>) = phase (s1\<lparr>pref := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>voronkov := uu1\<rparr>) = confIDs (s1\<lparr>voronkov := uu2\<rparr>) \<and> conf (s\<lparr>voronkov := uu1\<rparr>) = conf (s1\<lparr>voronkov := uu2\<rparr>) \<and> userIDs (s\<lparr>voronkov := uu1\<rparr>) = userIDs (s1\<lparr>voronkov := uu2\<rparr>) \<and> pass (s\<lparr>voronkov := uu1\<rparr>) = pass (s1\<lparr>voronkov := uu2\<rparr>) \<and> user (s\<lparr>voronkov := uu1\<rparr>) = user (s1\<lparr>voronkov := uu2\<rparr>) \<and> roles (s\<lparr>voronkov := uu1\<rparr>) = roles (s1\<lparr>voronkov := uu2\<rparr>) \<and> paperIDs (s\<lparr>voronkov := uu1\<rparr>) = paperIDs (s1\<lparr>voronkov := uu2\<rparr>) \<and> eeqExcPID2 (paper (s\<lparr>voronkov := uu1\<rparr>)) (paper (s1\<lparr>voronkov := uu2\<rparr>)) \<and> pref (s\<lparr>voronkov := uu1\<rparr>) = pref (s1\<lparr>voronkov := uu2\<rparr>) \<and> voronkov (s\<lparr>voronkov := uu1\<rparr>) = voronkov (s1\<lparr>voronkov := uu2\<rparr>) \<and> news (s\<lparr>voronkov := uu1\<rparr>) = news (s1\<lparr>voronkov := uu2\<rparr>) \<and> phase (s\<lparr>voronkov := uu1\<rparr>) = phase (s1\<lparr>voronkov := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>news := uu1\<rparr>) = confIDs (s1\<lparr>news := uu2\<rparr>) \<and> conf (s\<lparr>news := uu1\<rparr>) = conf (s1\<lparr>news := uu2\<rparr>) \<and> userIDs (s\<lparr>news := uu1\<rparr>) = userIDs (s1\<lparr>news := uu2\<rparr>) \<and> pass (s\<lparr>news := uu1\<rparr>) = pass (s1\<lparr>news := uu2\<rparr>) \<and> user (s\<lparr>news := uu1\<rparr>) = user (s1\<lparr>news := uu2\<rparr>) \<and> roles (s\<lparr>news := uu1\<rparr>) = roles (s1\<lparr>news := uu2\<rparr>) \<and> paperIDs (s\<lparr>news := uu1\<rparr>) = paperIDs (s1\<lparr>news := uu2\<rparr>) \<and> eeqExcPID2 (paper (s\<lparr>news := uu1\<rparr>)) (paper (s1\<lparr>news := uu2\<rparr>)) \<and> pref (s\<lparr>news := uu1\<rparr>) = pref (s1\<lparr>news := uu2\<rparr>) \<and> voronkov (s\<lparr>news := uu1\<rparr>) = voronkov (s1\<lparr>news := uu2\<rparr>) \<and> news (s\<lparr>news := uu1\<rparr>) = news (s1\<lparr>news := uu2\<rparr>) \<and> phase (s\<lparr>news := uu1\<rparr>) = phase (s1\<lparr>news := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1; uu1 = uu2\<rbrakk> \<Longrightarrow> confIDs (s\<lparr>phase := uu1\<rparr>) = confIDs (s1\<lparr>phase := uu2\<rparr>) \<and> conf (s\<lparr>phase := uu1\<rparr>) = conf (s1\<lparr>phase := uu2\<rparr>) \<and> userIDs (s\<lparr>phase := uu1\<rparr>) = userIDs (s1\<lparr>phase := uu2\<rparr>) \<and> pass (s\<lparr>phase := uu1\<rparr>) = pass (s1\<lparr>phase := uu2\<rparr>) \<and> user (s\<lparr>phase := uu1\<rparr>) = user (s1\<lparr>phase := uu2\<rparr>) \<and> roles (s\<lparr>phase := uu1\<rparr>) = roles (s1\<lparr>phase := uu2\<rparr>) \<and> paperIDs (s\<lparr>phase := uu1\<rparr>) = paperIDs (s1\<lparr>phase := uu2\<rparr>) \<and> eeqExcPID2 (paper (s\<lparr>phase := uu1\<rparr>)) (paper (s1\<lparr>phase := uu2\<rparr>)) \<and> pref (s\<lparr>phase := uu1\<rparr>) = pref (s1\<lparr>phase := uu2\<rparr>) \<and> voronkov (s\<lparr>phase := uu1\<rparr>) = voronkov (s1\<lparr>phase := uu2\<rparr>) \<and> news (s\<lparr>phase := uu1\<rparr>) = news (s1\<lparr>phase := uu2\<rparr>) \<and> phase (s\<lparr>phase := uu1\<rparr>) = phase (s1\<lparr>phase := uu2\<rparr>))
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcPID2_Paper:
assumes s's1': "eqExcPID2 s s1"
and "paper s pid = Paper title abstract content reviews dis decs"
and "paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1"
shows "title = title1 \<and> abstract = abstract1 \<and> content = content1 \<and> reviews = reviews1 \<and>
    dis = dis1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. title = title1 \<and> abstract = abstract1 \<and> content = content1 \<and> reviews = reviews1 \<and> dis = dis1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqExcPID2 s s1
paper s pid = Paper title abstract content reviews dis decs
paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1

goal (1 subgoal):
 1. title = title1 \<and> abstract = abstract1 \<and> content = content1 \<and> reviews = reviews1 \<and> dis = dis1
[PROOF STEP]
unfolding eqExcPID2_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> eeqExcPID2 (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1
paper s pid = Paper title abstract content reviews dis decs
paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1

goal (1 subgoal):
 1. title = title1 \<and> abstract = abstract1 \<and> content = content1 \<and> reviews = reviews1 \<and> dis = dis1
[PROOF STEP]
apply (auto simp: eqExcD2 eeqExcPID2_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>paper s pid = Paper title abstract content reviews dis decs; paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1; confIDs s = confIDs s1; conf s = conf s1; userIDs s = userIDs s1; pass s = pass s1; user s = user s1; roles s = roles s1; paperIDs s = paperIDs s1; \<forall>pid. (pid = PID \<longrightarrow> disPaper (paper s PID) = disPaper (paper s1 PID) \<and> reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and> contentPaper (paper s PID) = contentPaper (paper s1 PID) \<and> abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \<and> titlePaper (paper s PID) = titlePaper (paper s1 PID) \<and> hd (decsPaper (paper s PID)) = hd (decsPaper (paper s1 PID))) \<and> (pid = PID \<or> paper s pid = paper s1 pid); pref s = pref s1; voronkov s = voronkov s1; news s = news s1; phase s = phase s1\<rbrakk> \<Longrightarrow> title = title1
 2. \<lbrakk>paper s pid = Paper title abstract content reviews dis decs; paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1; confIDs s = confIDs s1; conf s = conf s1; userIDs s = userIDs s1; pass s = pass s1; user s = user s1; roles s = roles s1; paperIDs s = paperIDs s1; \<forall>pid. (pid = PID \<longrightarrow> disPaper (paper s PID) = disPaper (paper s1 PID) \<and> reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and> contentPaper (paper s PID) = contentPaper (paper s1 PID) \<and> abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \<and> titlePaper (paper s PID) = titlePaper (paper s1 PID) \<and> hd (decsPaper (paper s PID)) = hd (decsPaper (paper s1 PID))) \<and> (pid = PID \<or> paper s pid = paper s1 pid); pref s = pref s1; voronkov s = voronkov s1; news s = news s1; phase s = phase s1\<rbrakk> \<Longrightarrow> abstract = abstract1
 3. \<lbrakk>paper s pid = Paper title abstract content reviews dis decs; paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1; confIDs s = confIDs s1; conf s = conf s1; userIDs s = userIDs s1; pass s = pass s1; user s = user s1; roles s = roles s1; paperIDs s = paperIDs s1; \<forall>pid. (pid = PID \<longrightarrow> disPaper (paper s PID) = disPaper (paper s1 PID) \<and> reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and> contentPaper (paper s PID) = contentPaper (paper s1 PID) \<and> abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \<and> titlePaper (paper s PID) = titlePaper (paper s1 PID) \<and> hd (decsPaper (paper s PID)) = hd (decsPaper (paper s1 PID))) \<and> (pid = PID \<or> paper s pid = paper s1 pid); pref s = pref s1; voronkov s = voronkov s1; news s = news s1; phase s = phase s1\<rbrakk> \<Longrightarrow> content = content1
 4. \<lbrakk>paper s pid = Paper title abstract content reviews dis decs; paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1; confIDs s = confIDs s1; conf s = conf s1; userIDs s = userIDs s1; pass s = pass s1; user s = user s1; roles s = roles s1; paperIDs s = paperIDs s1; \<forall>pid. (pid = PID \<longrightarrow> disPaper (paper s PID) = disPaper (paper s1 PID) \<and> reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and> contentPaper (paper s PID) = contentPaper (paper s1 PID) \<and> abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \<and> titlePaper (paper s PID) = titlePaper (paper s1 PID) \<and> hd (decsPaper (paper s PID)) = hd (decsPaper (paper s1 PID))) \<and> (pid = PID \<or> paper s pid = paper s1 pid); pref s = pref s1; voronkov s = voronkov s1; news s = news s1; phase s = phase s1\<rbrakk> \<Longrightarrow> reviews = reviews1
 5. \<lbrakk>paper s pid = Paper title abstract content reviews dis decs; paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1; confIDs s = confIDs s1; conf s = conf s1; userIDs s = userIDs s1; pass s = pass s1; user s = user s1; roles s = roles s1; paperIDs s = paperIDs s1; \<forall>pid. (pid = PID \<longrightarrow> disPaper (paper s PID) = disPaper (paper s1 PID) \<and> reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and> contentPaper (paper s PID) = contentPaper (paper s1 PID) \<and> abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \<and> titlePaper (paper s PID) = titlePaper (paper s1 PID) \<and> hd (decsPaper (paper s PID)) = hd (decsPaper (paper s1 PID))) \<and> (pid = PID \<or> paper s pid = paper s1 pid); pref s = pref s1; voronkov s = voronkov s1; news s = news s1; phase s = phase s1\<rbrakk> \<Longrightarrow> dis = dis1
[PROOF STEP]
by (metis titlePaper.simps abstractPaper.simps contentPaper.simps reviewsPaper.simps
disPaper.simps)+


[STATEMENT]
lemma \<phi>_def2:
"\<phi> (Trans s a ou s') = (\<exists> cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1. a = Cact x1 \<Longrightarrow> \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
 2. \<And>x2. a = Uact x2 \<Longrightarrow> \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
 3. \<And>x3. a = UUact x3 \<Longrightarrow> \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
 4. \<And>x4. a = Ract x4 \<Longrightarrow> \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
 5. \<And>x5. a = Lact x5 \<Longrightarrow> \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
[PROOF STEP]
case (UUact x3)
[PROOF STATE]
proof (state)
this:
a = UUact x3

goal (5 subgoals):
 1. \<And>x1. a = Cact x1 \<Longrightarrow> \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
 2. \<And>x2. a = Uact x2 \<Longrightarrow> \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
 3. \<And>x3. a = UUact x3 \<Longrightarrow> \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
 4. \<And>x4. a = Ract x4 \<Longrightarrow> \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
 5. \<And>x5. a = Lact x5 \<Longrightarrow> \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
[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. \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
[PROOF STEP]
by (cases x3; auto)
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)

goal (4 subgoals):
 1. \<And>x1. a = Cact x1 \<Longrightarrow> \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
 2. \<And>x2. a = Uact x2 \<Longrightarrow> \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
 3. \<And>x4. a = Ract x4 \<Longrightarrow> \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
 4. \<And>x5. a = Lact x5 \<Longrightarrow> \<phi> (Trans s a ou s') = (\<exists>cid uid p dec. a = UUact (uuDec cid uid p PID dec) \<and> ou = outOK)
[PROOF STEP]
qed auto


[STATEMENT]
lemma UUact_uuDec_step_eqExcPID:
assumes a: "a = UUact (uuDec cid uid p PID dec)"
and "step s a = (ou,s')"
shows "eqExcPID s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID s s'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = UUact (uuDec cid uid p PID dec)
step s a = (ou, s')

goal (1 subgoal):
 1. eqExcPID s s'
[PROOF STEP]
unfolding eqExcPID_def eeqExcPID_def
[PROOF STATE]
proof (prove)
using this:
a = UUact (uuDec cid uid p PID dec)
step s a = (ou, s')

goal (1 subgoal):
 1. confIDs s = confIDs s' \<and> conf s = conf s' \<and> userIDs s = userIDs s' \<and> pass s = pass s' \<and> user s = user s' \<and> roles s = roles s' \<and> paperIDs s = paperIDs s' \<and> (\<forall>pid. if pid = PID then eqExcD (paper s pid) (paper s' pid) else paper s pid = paper s' pid) \<and> pref s = pref s' \<and> voronkov s = voronkov s' \<and> news s = news s' \<and> phase s = phase s'
[PROOF STEP]
by (auto simp: uu_defs)


[STATEMENT]
lemma \<phi>_step_eqExcPID:
assumes \<phi>: "\<phi> (Trans s a ou s')"
and s: "step s a = (ou,s')"
shows "eqExcPID s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID s s'
[PROOF STEP]
using \<phi> UUact_uuDec_step_eqExcPID[OF _ s]
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')
a = UUact (uuDec ?cid ?uid ?p PID ?dec) \<Longrightarrow> eqExcPID s s'

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

goal (1 subgoal):
 1. eqExcPID s s'
[PROOF STEP]
by blast