From 01c6c9f7b533d2df341cbf4ead2fe5a050069a5d Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@data61.csiro.au>
Date: Thu, 27 Jun 2019 18:41:28 +1000
Subject: [PATCH] riscv refine: weaken precondition of threadSet_invs_trivialT

---
 proof/refine/RISCV64/TcbAcc_R.thy | 1 -
 1 file changed, 1 deletion(-)

diff --git a/proof/refine/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy
index deb38c993..4878df897 100644
--- a/proof/refine/RISCV64/TcbAcc_R.thy
+++ b/proof/refine/RISCV64/TcbAcc_R.thy
@@ -1347,7 +1347,6 @@ lemma threadSet_invs_trivialT:
   assumes b: "\<forall>tcb. tcbMCP tcb \<le> maxPriority \<longrightarrow> tcbMCP (F tcb) \<le> maxPriority"
   shows
   "\<lbrace>\<lambda>s. invs' s \<and>
-       tcb_at' t s \<and>
        (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (F tcb)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))) \<and>
        (\<forall>ko d p. ko_at' ko t s \<and> inQ d p (F ko) \<and> \<not> inQ d p ko \<longrightarrow> t \<in> set (ksReadyQueues s (d, p))) \<and>
        ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (F tcb)) \<longrightarrow> ex_nonz_cap_to' t s \<and> t \<noteq> ksCurThread s) \<and>