--- a/Nominal/CPS/CPS3_DanvyFilinski.thy	Thu Jun 16 13:14:53 2011 +0100
+++ b/Nominal/CPS/CPS3_DanvyFilinski.thy	Thu Jun 16 21:23:38 2011 +0900
@@ -49,7 +49,6 @@
   apply simp
   apply (thin_tac "eqvt ka")
   apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "eqvt_at CPS1_CPS2_sumC (Inr (Ma, ca~))")
   apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))")
   prefer 2
   apply (simp add: Abs1_eq_iff')
@@ -130,9 +129,7 @@
   apply (simp add: fresh_def supp_at_base)
   apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
 --"-"
-  prefer 2
   apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "eqvt_at CPS1_CPS2_sumC (Inr (Ma, ca~))")
   apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))")
   prefer 2
   apply (simp add: Abs1_eq_iff')
@@ -212,11 +209,10 @@
   apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
   apply (simp add: fresh_def supp_at_base)
   apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
---"Only left subgoals are eqvt for the other side"
-  oops
+  done
 
-(*termination
-  sorry
+termination
+  by lexicographic_order
 
 definition psi:: "lt => lt"
   where "psi V == V*(\<lambda>x. x)"
@@ -237,7 +233,6 @@
   apply assumption
   apply rule
   done
-*)
 
 end