992     case vt_nil

   992     case vt_nil

   993     show "acyclic (RAG ([]::state))"

   993     show "acyclic (RAG ([]::state))"

   994       by (auto simp: s_RAG_def cs_waiting_def 

   994       by (auto simp: s_RAG_def cs_waiting_def 

   995         cs_holding_def wq_def acyclic_def)

   995         cs_holding_def wq_def acyclic_def)

   996 qed

   996 qed

   998 

   998 

   999 lemma finite_RAG: 

   999 lemma finite_RAG: 

  1000   fixes s

  1000   fixes s

  1001   assumes vt: "vt s"

  1001   assumes vt: "vt s"

  1002   shows "finite (RAG s)"

  1002   shows "finite (RAG s)"