--- a/Dynamic2static.thy	Mon Aug 05 12:30:26 2013 +0800
+++ b/Dynamic2static.thy	Tue Aug 27 08:50:53 2013 +0800
@@ -13,6 +13,9 @@
 apply 
 induct s, case tac e, every event analysis
 *)
+thm s2ss_def
+
+
 sorry
 
 lemma d2s_main':