equal
deleted
inserted
replaced
4655 assumes nxt: "next_th (s::event list) th cs th'" |
4655 assumes nxt: "next_th (s::event list) th cs th'" |
4656 shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s" |
4656 shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s" |
4657 using vt assms next_th_holding next_th_waiting |
4657 using vt assms next_th_holding next_th_waiting |
4658 by (unfold s_RAG_def, simp) |
4658 by (unfold s_RAG_def, simp) |
4659 |
4659 |
4660 end |
4660 end |
4661 |
4661 |
4662 end |
4662 context valid_trace_p |
|
4663 begin |
|
4664 |
|
4665 find_theorems readys th |
|
4666 |
|
4667 end |
|
4668 |
|
4669 end |