[STATEMENT]
lemma invarNT_K1exit: "invarNT (K1exit cid)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invarNT (K1exit cid)
[PROOF STEP]
unfolding invarNT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a ou s'. reachNT s \<and> K1exit cid s \<and> \<not> T (Trans s a ou s') \<and> step s a = (ou, s') \<longrightarrow> K1exit cid s'
[PROOF STEP]
apply (safe dest!: reachNT_reach)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s a ou s'. \<lbrakk>reach s; K1exit cid s; \<not> T (Trans s a ou s'); step s a = (ou, s')\<rbrakk> \<Longrightarrow> K1exit cid s'
[PROOF STEP]
subgoal for _ a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_)\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x2. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x3. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x4. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K1exit cid s'_
 5. \<And>x5. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply(cases x1)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14 x15. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cUser x11 x12 x13 x14 x15\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cConf x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x31 x32 x33 x34. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cPC x31 x32 x33 x34\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x41 x42 x43 x44. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cChair x41 x42 x43 x44\<rbrakk> \<Longrightarrow> K1exit cid s'_
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cPaper x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> K1exit cid s'_
 6. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cAuthor x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K1exit cid s'_
 7. \<And>x71 x72 x73 x74 x75. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cConflict x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> K1exit cid s'_
 8. \<And>x81 x82 x83 x84 x85. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cReview x81 x82 x83 x84 x85\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: c_defs K1exit_def geq_noPH_confIDs)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x3. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x4. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x5. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply(cases x2)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uUser x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x21 x22 x23. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uConfA x21 x22 x23\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x31 x32 x33 x34. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPhase x31 x32 x33 x34\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> K1exit cid s'_
 5. \<And>x51 x52 x53 x54 x55. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> K1exit cid s'_
 6. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K1exit cid s'_
 7. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uConfA x21 x22 x23\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x31 x32 x33 x34. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPhase x31 x32 x33 x34\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x51 x52 x53 x54 x55. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> K1exit cid s'_
 5. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K1exit cid s'_
 6. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x31 x32 x33 x34. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPhase x31 x32 x33 x34\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x51 x52 x53 x54 x55. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K1exit cid s'_
 5. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x51 x52 x53 x54 x55. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x51 x52 x53 x54 x55. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
subgoal for x61
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62_ x63_ x64_ x65_\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply(cases "x61 = cid")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62_ x63_ x64_ x65_; x61 = cid\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62_ x63_ x64_ x65_; x61 \<noteq> cid\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x4. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x5. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply(cases x3)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuNews x11 x12 x13 x14\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuDis x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x31 x32 x33 x34 x35 x36. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuReview x31 x32 x33 x34 x35 x36\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuDec x41 x42 x43 x44 x45\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: uu_defs K1exit_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x5. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done