--- a/no_shm_selinux/Finite_current.thy	Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Finite_current.thy	Tue Dec 31 14:57:13 2013 +0800
@@ -92,6 +92,12 @@
 apply (case_tac a, auto simp: init_finite_sets)
 done
 
+lemma maxium_queue:
+  "valid s \<Longrightarrow> length (msgs_of_queue s q) \<le> max_queue"
+apply (induct s) 
+apply (simp add:init_msgq_valid)
+apply (frule vt_grant_os, frule vd_cons, case_tac a, auto)
+done
 
 lemma finite_option: "finite {x. \<exists> y. f x = Some y} \<Longrightarrow> finite {y. \<exists> x. f x = Some y}"
 apply (drule_tac h = f in finite_imageI)