[STATEMENT]
lemma reachNT_non_isPC_isChair:
assumes "reachNT s" and "uid \<in> UIDs"
shows
"(PID \<in>\<in> paperIDs s cid \<and> isPC s cid uid \<and> phase s cid \<ge> disPH \<longrightarrow> pref s uid PID = Conflict) \<and>
 (PID \<in>\<in> paperIDs s cid \<and> isChair s cid uid \<and> phase s cid \<ge> disPH \<longrightarrow> pref s uid PID = Conflict)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (PID \<in>\<in> paperIDs s cid \<and> isPC s cid uid \<and> disPH \<le> phase s cid \<longrightarrow> pref s uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs s cid \<and> isChair s cid uid \<and> disPH \<le> phase s cid \<longrightarrow> pref s uid PID = Conflict)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachNT s
uid \<in> UIDs

goal (1 subgoal):
 1. (PID \<in>\<in> paperIDs s cid \<and> isPC s cid uid \<and> disPH \<le> phase s cid \<longrightarrow> pref s uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs s cid \<and> isChair s cid uid \<and> disPH \<le> phase s cid \<longrightarrow> pref s uid PID = Conflict)
[PROOF STEP]
apply induct
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. uid \<in> UIDs \<Longrightarrow> (PID \<in>\<in> paperIDs istate cid \<and> isPC istate cid uid \<and> disPH \<le> phase istate cid \<longrightarrow> pref istate uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs istate cid \<and> isChair istate cid uid \<and> disPH \<le> phase istate cid \<longrightarrow> pref istate uid PID = Conflict)
 2. \<And>trn. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isPC (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isChair (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> (PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isPC (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isChair (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict)
[PROOF STEP]
apply (auto simp: istate_def)[]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>trn. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isPC (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isChair (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> (PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isPC (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isChair (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict)
[PROOF STEP]
apply(intro conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>trn. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isPC (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isChair (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isPC (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict
 2. \<And>trn. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isPC (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isChair (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isChair (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict
[PROOF STEP]
subgoal for trn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isPC (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isChair (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isPC (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict
[PROOF STEP]
apply(cases trn, auto simp: T.simps reachNT_reach)[]
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>trn. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isPC (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isChair (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isChair (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict
[PROOF STEP]
by (metis T.elims(3) isChair_isPC reachNT_reach reach.Step tgtOf_simps)