[STATEMENT]
lemma eqExcPID_RDD:
"eqExcPID 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. eqExcPID 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 eqExcPID_imp eeqExcPID_RDD
[PROOF STATE]
proof (prove)
using this:
eqExcPID ?s ?s1.0 \<Longrightarrow> confIDs ?s = confIDs ?s1.0 \<and> conf ?s = conf ?s1.0 \<and> userIDs ?s = userIDs ?s1.0 \<and> pass ?s = pass ?s1.0 \<and> user ?s = user ?s1.0 \<and> roles ?s = roles ?s1.0 \<and> paperIDs ?s = paperIDs ?s1.0 \<and> eeqExcPID (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
eeqExcPID ?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)

goal (1 subgoal):
 1. eqExcPID 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