equal
deleted
inserted
replaced
404 show "finite {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}" |
404 show "finite {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}" |
405 proof - |
405 proof - |
406 have "{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)} = |
406 have "{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)} = |
407 the_thread ` {n . n \<in> subtree (RAG (t @ s)) (Th th) \<and> |
407 the_thread ` {n . n \<in> subtree (RAG (t @ s)) (Th th) \<and> |
408 (\<exists> th'. n = Th th')}" |
408 (\<exists> th'. n = Th th')}" |
409 by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps) |
409 by (force) |
410 moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) |
410 moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) |
411 ultimately show ?thesis by simp |
411 ultimately show ?thesis by simp |
412 qed |
412 qed |
413 next |
413 next |
414 show "th \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}" |
414 show "th \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}" |