diff -r 77daf1b85cf0 -r a5f5b9336007 thys2/Hoare_tm_basis.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Hoare_tm_basis.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,2857 @@
+header {* 
+  Separation logic for TM
+*}
+
+theory Hoare_tm_basis
+imports Hoare_gen My_block Data_slot MLs Term_pat (* BaseSS *) Subgoal Sort_ops
+        Thm_inst
+begin
+
+section {* Aux lemmas on seperation algebra *}
+
+lemma cond_eq: "((<b> \<and>* p) s) = (b \<and> (p s))"
+proof
+  assume "(<b> \<and>* p) s"
+  from condD[OF this] show " b \<and> p s" .
+next
+  assume "b \<and> p s"
+  hence b and "p s" by auto
+  from `b` have "(<b>) 0" by (auto simp:pasrt_def)
+  moreover have "s = 0 + s" by auto
+  moreover have "0 ## s" by auto
+  moreover note `p s`
+  ultimately show "(<b> \<and>* p) s" by (auto intro!:sep_conjI)
+qed
+
+lemma cond_eqI:
+  assumes h: "b \<Longrightarrow> r = s"
+  shows "(<b> ** r) = (<b> ** s)"
+proof(cases b)
+  case True
+  from h[OF this] show ?thesis by simp
+next
+  case False
+  thus ?thesis
+    by (unfold sep_conj_def set_ins_def pasrt_def, auto)
+qed
+
+lemma EXS_intro: 
+  assumes h: "(P x) s"
+  shows "((EXS x. P(x))) s"
+  by (smt h pred_ex_def sep_conj_impl)
+
+lemma EXS_elim: 
+  assumes "(EXS x. P x) s"
+  obtains x where "P x s"
+  by (metis assms pred_ex_def)
+
+lemma EXS_eq:
+  fixes x
+  assumes h: "Q (p x)" 
+  and h1: "\<And> y s. \<lbrakk>p y s\<rbrakk> \<Longrightarrow> y = x"
+  shows "p x = (EXS x. p x)"
+proof
+  fix s
+  show "p x s = (EXS x. p x) s"
+  proof
+    assume "p x s"
+    thus "(EXS x. p x) s" by (auto simp:pred_ex_def)
+  next
+    assume "(EXS x. p x) s"
+    thus "p x s"
+    proof(rule EXS_elim)
+      fix y
+      assume "p y s"
+      from this[unfolded h1[OF this]] show "p x s" .
+    qed
+  qed
+qed
+
+section {* The TM assembly language *}
+
+subsection {* The TM assembly language *}
+
+datatype taction = W0 | W1 | L | R
+
+datatype tstate = St nat
+
+fun nat_of :: "tstate \<Rightarrow> nat"
+where "nat_of (St n) = n"
+
+declare [[coercion_enabled]]
+
+declare [[coercion "St :: nat \<Rightarrow> tstate"]]
+
+type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)"
+
+datatype Block = Oc | Bk
+
+datatype tpg = 
+   TInstr tm_inst
+ | TLabel tstate
+ | TSeq tpg tpg
+ | TLocal "(tstate \<Rightarrow> tpg)"
+
+notation TLocal (binder "TL " 10)
+
+abbreviation tprog_instr :: "tm_inst \<Rightarrow> tpg" ("\<guillemotright> _" [61] 61)
+where "\<guillemotright> i \<equiv> TInstr i"
+
+abbreviation tprog_seq :: "tpg \<Rightarrow> tpg \<Rightarrow> tpg" (infixr ";" 52)
+where "c1 ; c2 \<equiv> TSeq c1 c2"
+
+subsection {* The notion of assembling *}
+
+datatype tresource = 
+    TM int Block
+  | TC nat tm_inst
+  | TAt nat
+  | TPos int
+  | TFaults nat
+
+type_synonym tassert = "tresource set \<Rightarrow> bool"
+
+definition "sg e = (\<lambda> s. s = e)"
+
+primrec tassemble_to :: "tpg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> tassert" 
+  where 
+  "tassemble_to (TInstr ai) i j = (sg ({TC i ai}) ** <(j = i + 1)>)" |
+  "tassemble_to (TSeq p1 p2) i j = (EXS j'. (tassemble_to p1 i j') ** (tassemble_to p2 j' j))" |
+  "tassemble_to (TLocal fp) i j  = (EXS l. (tassemble_to (fp l) i j))" | 
+  "tassemble_to (TLabel l) i j = <(i = j \<and> j = nat_of l)>"
+
+declare tassemble_to.simps [simp del]
+
+lemmas tasmp = tassemble_to.simps (2, 3, 4)
+
+abbreviation tasmb_to :: "nat \<Rightarrow> tpg \<Rightarrow> nat \<Rightarrow> tassert" ("_ :[ _ ]: _" [60, 60, 60] 60)
+  where "i :[ tpg ]: j \<equiv> tassemble_to tpg i j"
+
+section {* Automatic checking of assemblility *}
+
+subsection {* Basic theories *}
+
+text {* @{text cpg} is the type for skeleton assembly language. Every constructor
+        corresponds to one in the definition of @{text tpg} *}
+
+datatype cpg = 
+   CInstr tm_inst
+ | CLabel nat
+ | CSeq cpg cpg
+ | CLocal cpg
+
+text {* Conversion from @{text cpg} to @{text tpg}*}
+
+fun c2t :: "tstate list \<Rightarrow> cpg \<Rightarrow> tpg" where 
+  "c2t env (CInstr ((act0, St st0), (act1, St st1))) = 
+                         TInstr ((act0, env!st0), (act1, env!st1))" |
+  "c2t env (CLabel l) = TLabel (env!l)" |
+  "c2t env (CSeq cpg1 cpg2) = TSeq (c2t env cpg1) (c2t env cpg2)" |
+  "c2t env (CLocal cpg) = TLocal (\<lambda> x. c2t (x#env) cpg)"
+
+text {* Well formedness checking of @{text cpg} *}
+
+datatype status = Free | Bound
+
+text {* @{text wf_cpg_test} is the checking function *}
+
+fun  wf_cpg_test :: "status list \<Rightarrow> cpg \<Rightarrow> (bool \<times> status list)" where
+  "wf_cpg_test sts (CInstr ((a0, l0), (a1, l1))) = ((l0 < length sts \<and> l1 < length sts), sts)" |
+  "wf_cpg_test sts (CLabel l) = ((l < length sts) \<and> sts!l = Free, sts[l:=Bound])" |
+  "wf_cpg_test sts (CSeq c1 c2) = (let (b1, sts1) = wf_cpg_test sts c1;
+                                  (b2, sts2) = wf_cpg_test sts1 c2 in
+                                     (b1 \<and> b2, sts2))" |
+  "wf_cpg_test sts (CLocal body) = (let (b, sts') = (wf_cpg_test (Free#sts) body) in 
+                                   (b, tl sts'))"
+
+text {*
+  The meaning the following @{text "c2p"} has to be understood together with 
+  the following lemma @{text "wf_cpg_test_correct"}. The intended use of @{text "c2p"}
+  is when the elements of @{text "sts"} are all @{text "Free"}, in which case, 
+  the precondition on @{text "f"}, i.e. 
+       @{text "\<forall> x. ((length x = length sts \<and> 
+                                    (\<forall> k < length sts. sts!k = Bound \<longrightarrow> (x!k = f i k))"}
+  is trivially true. 
+*}
+definition 
+   "c2p sts i cpg j = 
+           (\<exists> f. \<forall> x. ((length x = length sts \<and> 
+                        (\<forall> k < length sts. sts!k = Bound \<longrightarrow> (x!k = f i k)))
+                   \<longrightarrow> (\<exists> s. (i:[(c2t x cpg)]:j) s)))"
+
+instantiation status :: order
+begin
+  definition less_eq_status_def: "((st1::status) \<le> st2) = (st1 = Free \<or> st2 = Bound)"
+  definition less_status_def: "((st1::status) < st2) = (st1 \<le> st2 \<and> st1 \<noteq> st2)"
+instance
+proof
+  fix x y 
+  show "(x < (y::status)) = (x \<le> y \<and> \<not> y \<le> x)"
+    by (metis less_eq_status_def less_status_def status.distinct(1))
+next
+  fix x show "x \<le> (x::status)"
+    by (metis (full_types) less_eq_status_def status.exhaust)
+next
+  fix x y z
+  assume "x \<le> y" "y \<le> (z::status)" show "x \<le> (z::status)"
+    by (metis `x \<le> y` `y \<le> z` less_eq_status_def status.distinct(1))
+next
+  fix x y
+  assume "x \<le> y" "y \<le> (x::status)" show "x = y"
+    by (metis `x \<le> y` `y \<le> x` less_eq_status_def status.distinct(1))
+qed
+end
+
+instantiation list :: (order)order
+begin
+  definition "((sts::('a::order) list)  \<le> sts') = 
+                   ((length sts = length sts') \<and> (\<forall> i < length sts. sts!i \<le> sts'!i))"
+  definition "((sts::('a::order) list)  < sts') = ((sts \<le> sts') \<and> sts \<noteq> sts')"
+
+  lemma anti_sym: assumes h: "x \<le> (y::'a list)" "y \<le> x"
+      shows "x = y"
+  proof -
+    from h have "length x = length y"
+      by (metis less_eq_list_def)
+    moreover from h have " (\<forall> i < length x. x!i = y!i)"
+      by (metis (full_types) antisym_conv less_eq_list_def)
+    ultimately show ?thesis
+      by (metis nth_equalityI)
+  qed
+
+  lemma refl: "x \<le> (x::('a::order) list)"
+    apply (unfold less_eq_list_def)
+    by (metis order_refl)
+
+  instance
+  proof
+    fix x y
+    show "((x::('a::order) list) < y) = (x \<le> y \<and> \<not> y \<le> x)"
+    proof
+      assume h: "x \<le> y \<and> \<not> y \<le> x"
+      have "x \<noteq> y"
+      proof
+        assume "x = y" with h have "\<not> (x \<le> x)" by simp
+        with refl show False by auto
+      qed
+      moreover from h have "x \<le> y" by blast
+      ultimately show "x < y" by (auto simp:less_list_def)
+    next
+      assume h: "x < y"
+      hence hh: "x \<le> y"
+        by (metis less_list_def)
+      moreover have "\<not> y \<le> x"
+      proof
+        assume "y \<le> x"
+        from anti_sym[OF hh this] have "x = y" .
+        with h show False
+          by (metis less_list_def) 
+      qed
+      ultimately show "x \<le> y \<and> \<not> y \<le> x" by auto
+    qed
+  next
+    fix x from refl show "(x::'a list) \<le> x" .
+  next
+    fix x y assume "(x::'a list) \<le> y" "y \<le> x" 
+    from anti_sym[OF this] show "x = y" .
+  next
+    fix x y z
+    assume h: "(x::'a list) \<le> y" "y \<le> z"
+    show "x \<le> z"
+    proof -
+      from h have "length x = length z" by (metis less_eq_list_def)
+      moreover from h have "\<forall> i < length x. x!i \<le> z!i"
+        by (metis less_eq_list_def order_trans)
+      ultimately show "x \<le> z"
+        by (metis less_eq_list_def)
+    qed
+  qed
+end
+
+lemma sts_bound_le: "sts \<le> sts[l := Bound]"
+proof -
+  have "length sts = length (sts[l := Bound])"
+    by (metis length_list_update)
+  moreover have "\<forall> i < length sts. sts!i \<le> (sts[l:=Bound])!i"
+  proof -
+    { fix i
+      assume "i < length sts"
+      have "sts ! i \<le> sts[l := Bound] ! i"
+      proof(cases "l < length sts")
+        case True
+        note le_l = this
+        show ?thesis
+        proof(cases "l = i")
+          case True with le_l
+          have "sts[l := Bound] ! i = Bound" by auto
+          thus ?thesis by (metis less_eq_status_def) 
+        next
+          case False
+          with le_l have "sts[l := Bound] ! i = sts!i" by auto
+          thus ?thesis by auto
+        qed
+      next
+        case False
+        hence "sts[l := Bound] = sts" by auto
+        thus ?thesis by auto
+      qed
+    } thus ?thesis by auto
+  qed
+  ultimately show ?thesis by (metis less_eq_list_def) 
+qed
+
+lemma sts_tl_le:
+  assumes "sts \<le> sts'"
+  shows "tl sts \<le> tl sts'"
+proof -
+  from assms have "length (tl sts) = length (tl sts')"
+    by (metis (hide_lams, no_types) length_tl less_eq_list_def)
+  moreover from assms have "\<forall> i < length (tl sts). (tl sts)!i \<le> (tl sts')!i"
+    by (smt calculation length_tl less_eq_list_def nth_tl)
+  ultimately show ?thesis
+    by (metis less_eq_list_def)
+qed
+
+lemma wf_cpg_test_le:
+  assumes "wf_cpg_test sts cpg = (True, sts')"
+  shows "sts \<le> sts'" using assms
+proof(induct cpg arbitrary:sts sts')
+  case (CInstr instr sts sts')
+  obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, St l0), (a1, St l1))"
+    by (metis surj_pair tstate.exhaust)
+  from CInstr[unfolded this]
+  show ?case by simp
+next
+  case (CLabel l sts sts')
+  thus ?case by (auto simp:sts_bound_le)
+next
+  case (CLocal body sts sts')
+  from this(2)
+  obtain sts1 where h: "wf_cpg_test (Free # sts) body = (True, sts1)" "sts' = tl sts1"
+    by (auto split:prod.splits)
+  from CLocal(1)[OF this(1)] have "Free # sts \<le> sts1" .
+  from sts_tl_le[OF this]
+  have "sts \<le> tl sts1" by simp
+  from this[folded h(2)]
+  show ?case .
+next
+  case (CSeq cpg1 cpg2 sts sts')
+  from this(3)
+  show ?case
+    by (auto split:prod.splits dest!:CSeq(1, 2))
+qed
+
+lemma c2p_assert:
+  assumes "(c2p [] i cpg j)"
+  shows "\<exists> s. (i :[(c2t [] cpg)]: j) s"
+proof -
+  from assms obtain f where
+    h [rule_format]: 
+    "\<forall> x. length x = length [] \<and> (\<forall>k<length []. [] ! k = Bound \<longrightarrow> (x ! k = f i k)) \<longrightarrow>
+                        (\<exists> s. (i :[ c2t [] cpg ]: j) s)"
+    by (unfold c2p_def, auto)
+  have "length [] = length [] \<and> (\<forall>k<length []. [] ! k = Bound \<longrightarrow> ([] ! k = f i k))"
+    by auto
+  from h[OF this] obtain s where "(i :[ c2t [] cpg ]: j) s" by blast
+  thus ?thesis by auto
+qed
+
+definition "sts_disj sts sts' = ((length sts = length sts') \<and> 
+                                 (\<forall> i < length sts. \<not>(sts!i = Bound \<and> sts'!i = Bound)))"
+
+instantiation list :: (plus)plus
+begin
+   fun plus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+     "plus_list [] ys = []" |
+     "plus_list (x#xs) [] = []" |
+     "plus_list (x#xs) (y#ys) = ((x + y)#plus_list xs ys)"
+   instance ..
+end
+
+instantiation list :: (minus)minus
+begin
+   fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+     "minus_list [] ys = []" |
+     "minus_list (x#xs) [] = []" |
+     "minus_list (x#xs) (y#ys) = ((x - y)#minus_list xs ys)"
+   instance ..
+end
+
+instantiation status :: minus
+begin
+   fun minus_status :: "status \<Rightarrow> status \<Rightarrow> status" where
+     "minus_status Bound Bound = Free" |
+     "minus_status Bound Free = Bound" |
+     "minus_status Free x = Free "
+   instance ..
+end
+
+instantiation status :: plus
+begin
+   fun plus_status :: "status \<Rightarrow> status \<Rightarrow> status" where
+     "plus_status Free x = x" |
+     "plus_status Bound x = Bound"
+   instance ..
+end
+
+lemma length_sts_plus:
+  assumes "length (sts1 :: status list) = length sts2"
+  shows "length (sts1 + sts2) = length sts1"
+  using assms
+proof(induct sts1 arbitrary: sts2)
+  case Nil
+  thus ?case
+    by (metis plus_list.simps(1))
+next
+  case (Cons s' sts' sts2)
+  thus ?case
+  proof(cases "sts2 = []")
+    case True
+    with Cons show ?thesis by auto
+  next
+    case False
+    then obtain s'' sts'' where eq_sts2: "sts2 = s''#sts''"
+      by (metis neq_Nil_conv)
+    with Cons
+    show ?thesis
+      by (metis length_Suc_conv list.inject plus_list.simps(3))
+  qed
+qed
+
+lemma nth_sts_plus:
+  assumes "i < length ((sts1::status list) + sts2)"
+  shows "(sts1 + sts2)!i = sts1!i + sts2!i"
+  using assms
+proof(induct sts1 arbitrary:i sts2)
+  case (Nil i sts2)
+  thus ?case by auto
+next
+  case (Cons s' sts' i sts2)
+  show ?case
+  proof(cases "sts2 = []")
+    case True
+    with Cons show ?thesis by auto
+  next
+    case False
+    then obtain s'' sts'' where eq_sts2: "sts2 = s''#sts''"
+      by (metis neq_Nil_conv)
+    with Cons
+    show ?thesis
+      by (smt list.size(4) nth_Cons' plus_list.simps(3))
+  qed
+qed
+
+lemma nth_sts_minus:
+  assumes "i < length ((sts1::status list) - sts2)"
+  shows "(sts1 - sts2)!i = sts1!i - sts2!i"
+  using assms
+proof(induct  arbitrary:i rule:minus_list.induct)
+  case (3 x xs y ys i)
+  show ?case
+  proof(cases i)
+    case 0
+    thus ?thesis by simp
+  next
+    case (Suc k)
+    with 3(2) have "k < length (xs - ys)" by auto
+    from 3(1)[OF this] and Suc
+    show ?thesis
+      by auto
+  qed
+qed auto
+
+fun taddr :: "tresource \<Rightarrow> nat" where
+   "taddr (TC i instr) = i"
+
+lemma tassemble_to_range:
+  assumes "(i :[tpg]: j) s"
+  shows "(i \<le> j) \<and> (\<forall> r \<in> s. i \<le> taddr r \<and> taddr r < j)"
+  using assms
+proof(induct tpg arbitrary: i j s)
+  case (TInstr instr i j s)
+  obtain a0 l0 a1 l1 where "instr = ((a0, l0), (a1, l1))"
+    by (metis pair_collapse)
+  with TInstr
+  show ?case
+    apply (simp add:tassemble_to.simps sg_def)
+    by (smt `instr = ((a0, l0), a1, l1)` cond_eq cond_true_eq1 
+        empty_iff insert_iff le_refl lessI sep.mult_commute taddr.simps)
+next
+  case (TLabel l i j s)
+  thus ?case
+    apply (simp add:tassemble_to.simps)
+    by (smt equals0D pasrt_def set_zero_def)
+next
+  case (TSeq c1 c2 i j s)
+  from TSeq(3) obtain s1 s2 j' where 
+    h: "(i :[ c1 ]: j') s1" "(j' :[ c2 ]: j) s2" "s1 ## s2" "s = s1 + s2"
+    by (auto simp:tassemble_to.simps elim!:EXS_elim sep_conjE)
+  show ?case
+  proof -
+    { fix r 
+      assume "r \<in> s"
+      with h (3, 4) have "r \<in> s1 \<or> r \<in> s2"
+        by (auto simp:set_ins_def)
+      hence "i \<le> j \<and> i \<le> taddr r \<and> taddr r < j" 
+      proof
+        assume " r \<in> s1"
+        from TSeq(1)[OF h(1)]
+        have "i \<le> j'" "(\<forall>r\<in>s1. i \<le> taddr r \<and> taddr r < j')" by auto
+        from this(2)[rule_format, OF `r \<in> s1`]
+        have "i \<le> taddr r" "taddr r < j'" by auto
+        with TSeq(2)[OF h(2)]
+        show ?thesis by auto
+      next
+        assume "r \<in> s2"
+        from TSeq(2)[OF h(2)]
+        have "j' \<le> j" "(\<forall>r\<in>s2. j' \<le> taddr r \<and> taddr r < j)" by auto
+        from this(2)[rule_format, OF `r \<in> s2`]
+        have "j' \<le> taddr r" "taddr r < j" by auto
+        with TSeq(1)[OF h(1)]
+        show ?thesis by auto
+      qed
+    } thus ?thesis
+      by (smt TSeq.hyps(1) TSeq.hyps(2) h(1) h(2))
+  qed
+next
+  case (TLocal body i j s)
+  from this(2) obtain l s' where "(i :[ body l ]: j) s"
+    by (simp add:tassemble_to.simps, auto elim!:EXS_elim)
+  from TLocal(1)[OF this]
+  show ?case by auto
+qed
+
+lemma c2p_seq:
+  assumes "c2p sts1 i cpg1 j'"
+          "c2p sts2 j' cpg2 j"
+          "sts_disj sts1 sts2"
+  shows "(c2p (sts1 + sts2) i (CSeq cpg1 cpg2) j)" 
+proof -
+  from assms(1)[unfolded c2p_def]
+  obtain f1 where
+    h1[rule_format]: 
+        "\<forall>x. length x = length sts1 \<and> (\<forall>k<length sts1. sts1 ! k = Bound \<longrightarrow> (x ! k = f1 i k)) \<longrightarrow>
+              Ex (i :[ c2t x cpg1 ]: j')" by blast
+  from assms(2)[unfolded c2p_def]
+  obtain f2 where h2[rule_format]: 
+        "\<forall>x. length x = length sts2 \<and> (\<forall>k<length sts2. sts2 ! k = Bound \<longrightarrow> (x ! k = f2 j' k)) \<longrightarrow>
+              Ex (j' :[ c2t x cpg2 ]: j)" by blast
+  from assms(3)[unfolded sts_disj_def]
+  have h3: "length sts1 = length sts2" 
+    and h4[rule_format]: 
+        "(\<forall>i<length sts1. \<not> (sts1 ! i = Bound \<and> sts2 ! i = Bound))" by auto
+  let ?f = "\<lambda> i k. if (sts1!k = Bound) then f1 i k else f2 j' k"
+  { fix x 
+    assume h5: "length x = length (sts1 + sts2)" and
+           h6[rule_format]: "(\<forall>k<length (sts1 + sts2). (sts1 + sts2) ! k = Bound \<longrightarrow> x ! k = ?f i k)"
+    obtain s1 where h_s1: "(i :[ c2t x cpg1 ]: j') s1"
+    proof(atomize_elim, rule h1)
+      from h3 h5 have "length x = length sts1"
+        by (metis length_sts_plus)
+      moreover {
+        fix k assume hh: "k<length sts1" "sts1 ! k = Bound"
+        from hh(1) h3 h5 have p1: "k < length (sts1 + sts2)"
+          by (metis calculation)
+        from h3 hh(2) have p2: "(sts1 + sts2)!k = Bound"
+          by (metis nth_sts_plus p1 plus_status.simps(2))
+        from h6[OF p1 p2] have "x ! k = (if sts1 ! k = Bound then f1 i k else f2 j' k)" .
+        with hh(2)
+        have "x ! k = f1 i k" by simp
+      } ultimately show "length x = length sts1 \<and> 
+          (\<forall>k<length sts1. sts1 ! k = Bound \<longrightarrow> (x ! k = f1 i k))"
+        by blast
+    qed
+    obtain s2 where h_s2: "(j' :[ c2t x cpg2 ]: j) s2"
+    proof(atomize_elim, rule h2)
+      from h3 h5 have "length x = length sts2"
+        by (metis length_sts_plus) 
+      moreover {
+        fix k
+        assume hh: "k<length sts2" "sts2 ! k = Bound"
+        from hh(1) h3 h5 have p1: "k < length (sts1 + sts2)"
+          by (metis calculation)
+        from  hh(1) h3 h5 hh(2) have p2: "(sts1 + sts2)!k = Bound"
+          by (metis `length sts1 = length sts2 \<and> 
+               (\<forall>i<length sts1. \<not> (sts1 ! i = Bound \<and> sts2 ! i = Bound))` 
+             calculation nth_sts_plus plus_status.simps(1) status.distinct(1) status.exhaust)
+        from h6[OF p1 p2] have "x ! k = (if sts1 ! k = Bound then f1 i k else f2 j' k)" .
+        moreover from h4[OF hh(1)[folded h3]] hh(2) have "sts1!k \<noteq> Bound" by auto
+        ultimately have "x!k = f2 j' k" by simp
+      } ultimately show "length x = length sts2 \<and> 
+                               (\<forall>k<length sts2. sts2 ! k = Bound \<longrightarrow> (x ! k = f2 j' k))"
+        by blast
+    qed
+    have h_s12: "s1 ## s2"
+    proof -
+      { fix r assume h: "r \<in> s1" "r \<in> s2"
+        with h_s1 h_s2
+        have "False"by (smt tassemble_to_range) 
+      } thus ?thesis by (auto simp:set_ins_def)
+    qed  
+    have "(EXS j'. i :[ c2t x cpg1 ]: j' \<and>* j' :[ c2t x cpg2 ]: j) (s1 + s2)"
+    proof(rule_tac x = j' in EXS_intro)
+      from h_s1 h_s2 h_s12
+      show "(i :[ c2t x cpg1 ]: j' \<and>* j' :[ c2t x cpg2 ]: j) (s1 + s2)"
+        by (metis sep_conjI)
+    qed
+    hence "\<exists> s. (i :[ c2t x (CSeq cpg1 cpg2) ]: j) s" 
+      by (auto simp:tassemble_to.simps)
+  }
+  hence "\<exists>f. \<forall>x. length x = length (sts1 + sts2) \<and>
+               (\<forall>k<length (sts1 + sts2). (sts1 + sts2) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow>
+               Ex (i :[ c2t x (CSeq cpg1 cpg2) ]: j)"
+    by (rule_tac x = ?f in exI, auto)
+  thus ?thesis 
+    by(unfold c2p_def, auto)
+qed
+
+lemma plus_list_len:
+  "length ((sts1::status list) + sts2) = min (length sts1) (length sts2)"
+  by(induct rule:plus_list.induct, auto)
+
+lemma minus_list_len:
+  "length ((sts1::status list) - sts2) = min (length sts1) (length sts2)"
+  by(induct rule:minus_list.induct, auto)
+
+lemma sts_le_comb:
+  assumes "sts1 \<le> sts2"
+  and "sts2 \<le> sts3"
+  shows "sts_disj (sts2 - sts1) (sts3 - sts2)" and
+        "(sts3 - sts1) = (sts2 - sts1) + (sts3 - sts2)"
+proof -
+  from assms 
+  have h1: "length sts1 = length sts2" "\<forall>i<length sts1. sts1 ! i \<le> sts2 ! i"
+    and h2: "length sts2 = length sts3" "\<forall>i<length sts1. sts2 ! i \<le> sts3 ! i"
+    by (unfold less_eq_list_def, auto)
+  have "sts_disj (sts2 - sts1) (sts3 - sts2)"
+  proof -
+    from h1(1) h2(1)
+    have "length (sts2 - sts1) = length (sts3 - sts2)"
+      by (metis minus_list_len)
+    moreover {
+      fix i
+      assume lt_i: "i<length (sts2 - sts1)"
+      from lt_i h1(1) h2(1) have "i < length sts1"
+        by (smt minus_list_len)
+      from h1(2)[rule_format, of i, OF this] h2(2)[rule_format, of i, OF this]
+      have "sts1 ! i \<le> sts2 ! i" "sts2 ! i \<le> sts3 ! i" .
+      moreover have "(sts2 - sts1) ! i = sts2!i - sts1!i"
+        by (metis lt_i nth_sts_minus)
+      moreover have "(sts3 - sts2)!i = sts3!i - sts2!i"
+        by (metis `length (sts2 - sts1) = length (sts3 - sts2)` lt_i nth_sts_minus)
+      ultimately have " \<not> ((sts2 - sts1) ! i = Bound \<and> (sts3 - sts2) ! i = Bound)"
+        apply (cases "sts2!i", cases "sts1!i", cases "sts3!i", simp, simp)
+        apply (cases "sts3!i", simp, simp)
+        apply (cases "sts1!i", cases "sts3!i", simp, simp)
+        by (cases "sts3!i", simp, simp)
+    } ultimately show ?thesis by (unfold sts_disj_def, auto)
+  qed
+  moreover have "(sts3 - sts1) = (sts2 - sts1) + (sts3 - sts2)"
+  proof(induct rule:nth_equalityI)
+    case 1
+    show ?case by (metis h1(1) h2(1) length_sts_plus minus_list_len)
+  next 
+    case 2
+    { fix i
+      assume lt_i: "i<length (sts3 - sts1)"
+      have "(sts3 - sts1) ! i = (sts2 - sts1 + (sts3 - sts2)) ! i" (is "?L = ?R")
+      proof -
+        have "?R = sts2!i - sts1!i + (sts3!i - sts2!i)"
+          by (smt `i < length (sts3 - sts1)` h2(1) minus_list_len nth_sts_minus 
+                   nth_sts_plus plus_list_len)
+        moreover have "?L = sts3!i - sts1!i"
+          by (metis `i < length (sts3 - sts1)` nth_sts_minus)
+        moreover 
+        have "sts2!i - sts1!i + (sts3!i - sts2!i) = sts3!i - sts1!i"
+        proof -
+          from lt_i h1(1) h2(1) have "i < length sts1"
+            by (smt minus_list_len)
+          from h1(2)[rule_format, of i, OF this] h2(2)[rule_format, of i, OF this]
+          show ?thesis
+            apply (cases "sts2!i", cases "sts1!i", cases "sts3!i", simp, simp)
+            apply (cases "sts3!i", simp, simp)
+            apply (cases "sts1!i", cases "sts3!i", simp, simp)
+            by (cases "sts3!i", simp, simp)
+        qed
+        ultimately show ?thesis by simp
+      qed
+    } thus ?case by auto
+  qed
+  ultimately show "sts_disj (sts2 - sts1) (sts3 - sts2)" and
+                  "(sts3 - sts1) = (sts2 - sts1) + (sts3 - sts2)" by auto
+qed
+
+lemma wf_cpg_test_correct: 
+  assumes "wf_cpg_test sts cpg = (True, sts')"
+  shows "(\<forall> i. \<exists> j. (c2p (sts' - sts) i cpg j))" 
+  using assms
+proof(induct cpg arbitrary:sts sts')
+  case (CInstr instr sts sts')
+  obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, St l0), (a1, St l1))"
+    by (metis surj_pair tstate.exhaust)
+  show ?case 
+  proof(unfold eq_instr c2p_def, clarsimp simp:tassemble_to.simps)
+    fix i
+    let ?a = "(Suc i)" and ?f = "\<lambda> i k. St i"
+    show "\<exists>a f. \<forall>x. length x = length (sts' - sts) \<and>
+                  (\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow>
+                  Ex (sg {TC i ((a0, (x ! l0)), a1, (x ! l1))} \<and>* <(a = (Suc i))>)"
+    proof(rule_tac x = ?a in exI, rule_tac x = ?f in exI, default, clarsimp)
+      fix x
+      let ?j = "Suc i"
+      let ?s = " {TC i ((a0, x ! l0), a1, x ! l1)}"
+      have "(sg {TC i ((a0, x ! l0), a1, x ! l1)} \<and>* <(Suc i = Suc i)>) ?s"
+        by (simp add:tassemble_to.simps sg_def)
+      thus "Ex (sg {TC i ((a0, (x ! l0)), a1, (x ! l1))})"
+        by auto
+    qed
+  qed
+next
+  case (CLabel l sts sts')
+  show ?case
+  proof
+    fix i
+    from CLabel 
+    have h1: "l < length sts" 
+      and h2: "sts ! l = Free"
+      and h3: "sts[l := Bound] = sts'" by auto
+    let ?f = "\<lambda> i k. St i"
+    have "\<exists>a f. \<forall>x. length x = length (sts' - sts) \<and>
+                  (\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f (i::nat) k) \<longrightarrow>
+                  Ex (<(i = a \<and> a = nat_of (x ! l))>)"
+    proof(rule_tac x = i in exI, rule_tac x = ?f in exI, clarsimp)
+      fix x
+      assume h[rule_format]:
+        "\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = St i"
+      from h1 h3 have p1: "l < length (sts' - sts)"
+        by (metis length_list_update min_max.inf.idem minus_list_len)
+      from p1 h2 h3 have p2: "(sts' - sts)!l = Bound"
+        by (metis h1 minus_status.simps(2) nth_list_update_eq nth_sts_minus)
+      from h[OF p1 p2] have "(<(i = nat_of (x ! l))>) 0" 
+        by (simp add:set_ins_def)
+      thus "\<exists> s.  (<(i = nat_of (x ! l))>) s" by auto
+    qed 
+    thus "\<exists>a. c2p (sts' - sts) i (CLabel l) a"
+      by (auto simp:c2p_def tassemble_to.simps)
+  qed
+next
+  case (CSeq cpg1 cpg2 sts sts')
+  show ?case
+  proof
+    fix i
+    from CSeq(3)[unfolded wf_cpg_test.simps]
+    obtain b1 sts1
+    where LetE: "(let (b2, y) = wf_cpg_test sts1 cpg2 in (b1 \<and> b2, y)) = (True, sts')"
+          "(b1, sts1) = wf_cpg_test sts cpg1"
+      by (auto simp:Let_def split:prod.splits)
+    show "\<exists> j. c2p (sts' - sts) i (CSeq cpg1 cpg2) j"
+    proof -
+      from LetE(1)
+      obtain b2 where h: "(b2, sts') = wf_cpg_test sts1 cpg2" "b1=True" "b2=True" 
+        by (atomize_elim, unfold Let_def, auto split:prod.splits)
+      from wf_cpg_test_le[OF LetE(2)[symmetric, unfolded h(2)]]
+      have sts_le1: "sts \<le> sts1" .
+      from CSeq(1)[OF LetE(2)[unfolded h(2), symmetric], rule_format, of i]
+      obtain j1 where h1: "(c2p (sts1 - sts) i cpg1 j1)" by blast
+      from wf_cpg_test_le[OF h(1)[symmetric, unfolded h(3)]]
+      have sts_le2: "sts1 \<le> sts'" .
+      from sts_le_comb[OF sts_le1 sts_le2]
+      have hh: "sts_disj (sts1 - sts) (sts' - sts1)"
+               "sts' - sts = (sts1 - sts) + (sts' - sts1)" .
+      from CSeq(2)[OF h(1)[symmetric, unfolded h(3)], rule_format, of j1]
+      obtain j2 where h2: "(c2p (sts' - sts1) j1 cpg2 j2)" by blast
+      have "c2p (sts' - sts) i (CSeq cpg1 cpg2) j2"
+        by(unfold hh(2), rule c2p_seq[OF h1 h2 hh(1)])
+      thus ?thesis by blast 
+    qed
+  qed
+next
+  case (CLocal body sts sts')
+  from this(2) obtain b sts1 s where 
+      h: "wf_cpg_test (Free # sts) body = (True, sts1)"
+         "sts' = tl sts1" 
+    by (unfold wf_cpg_test.simps, auto split:prod.splits)
+  from wf_cpg_test_le[OF h(1), unfolded less_eq_list_def] h(2)
+  obtain s where eq_sts1: "sts1 = s#sts'"
+    by (metis Suc_length_conv list.size(4) tl.simps(2))
+  from CLocal(1)[OF h(1)] have p1: "\<forall>i. \<exists>a. c2p (sts1 - (Free # sts)) i body a" .
+  show ?case
+  proof
+    fix i
+    from p1[rule_format, of i] obtain j where "(c2p (sts1 - (Free # sts)) i body) j" by blast
+    then obtain f where hh [rule_format]: 
+           "\<forall>x. length x = length (sts1 - (Free # sts)) \<and>
+                (\<forall>k<length (sts1 - (Free # sts)). (sts1 - (Free # sts)) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow>
+                        (\<exists>s. (i :[ c2t x body ]: j) s)"
+      by (auto simp:c2p_def)
+    let ?f = "\<lambda> i k. f i (Suc k)"
+    have "\<exists>j f. \<forall>x. length x = length (sts' - sts) \<and>
+              (\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow>
+          (\<exists>s. (i :[ (TL xa. c2t (xa # x) body) ]: j) s)"
+    proof(rule_tac x = j in exI, rule_tac x = ?f in exI, default, clarsimp)
+      fix x
+      assume h1: "length x = length (sts' - sts)"
+        and h2: "\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f i (Suc k)"
+      let ?l = "f i 0" let ?x = " ?l#x"
+      from wf_cpg_test_le[OF h(1)] have "length (Free#sts) = length sts1"
+        by (unfold less_eq_list_def, simp)
+      with h1 h(2) have q1: "length (?l # x) = length (sts1 - (Free # sts))"
+        by (smt Suc_length_conv length_Suc_conv list.inject list.size(4) 
+                minus_list.simps(3) minus_list_len tl.simps(2))
+      have q2: "(\<forall>k<length (sts1 - (Free # sts)). 
+                  (sts1 - (Free # sts)) ! k = Bound \<longrightarrow> (f i 0 # x) ! k = f i k)" 
+      proof -
+        { fix k
+          assume lt_k: "k<length (sts1 - (Free # sts))"
+            and  bd_k: "(sts1 - (Free # sts)) ! k = Bound"
+          have "(f i 0 # x) ! k = f i k"
+          proof(cases "k")
+            case (Suc k')
+            moreover have "x ! k' = f i (Suc k')"
+            proof(rule h2[rule_format])
+              from bd_k Suc eq_sts1 show "(sts' - sts) ! k' = Bound" by simp
+            next
+              from Suc lt_k eq_sts1 show "k' < length (sts' - sts)" by simp
+            qed
+            ultimately show ?thesis by simp
+          qed simp
+        } thus ?thesis by auto
+      qed
+      from conjI[THEN hh[of ?x], OF q1 q2] obtain s 
+        where h_s: "(i :[ c2t (f i 0 # x) body ]: j) s" by blast
+      thus "(\<exists>s. (i :[ (TL xa. c2t (xa # x) body) ]: j) s)"
+        apply (simp add:tassemble_to.simps)
+        by (rule_tac x = s in exI, rule_tac x = "?l::tstate" in EXS_intro, simp)
+    qed
+    thus "\<exists>j. c2p (sts' - sts) i (CLocal body) j" 
+      by (auto simp:c2p_def)
+  qed
+qed
+
+lemma 
+  assumes "wf_cpg_test [] cpg = (True, sts')"
+  and "tpg = c2t [] cpg"
+  shows "\<forall> i. \<exists> j s.  ((i:[tpg]:j) s)"
+proof
+  fix i
+  have eq_sts_minus: "(sts' - []) = []"
+    by (metis list.exhaust minus_list.simps(1) minus_list.simps(2))
+  from wf_cpg_test_correct[OF assms(1), rule_format, of i]
+  obtain j where "c2p (sts' - []) i cpg j" by auto
+  from c2p_assert [OF this[unfolded eq_sts_minus]]
+  obtain s where "(i :[ c2t [] cpg ]: j) s" by blast
+  from this[folded assms(2)]
+  show " \<exists> j s.  ((i:[tpg]:j) s)" by blast
+qed
+
+lemma replicate_nth: "(replicate n x @ sts) ! (l + n)  = sts!l"
+  by (smt length_replicate nth_append)
+
+lemma replicate_update: 
+  "(replicate n x @ sts)[l + n := v] = replicate n x @ sts[l := v]"
+  by (smt length_replicate list_update_append)
+
+lemma nth_app: "length xs \<le> a \<Longrightarrow> (xs @ ys)!a = ys!(a - length xs)"
+  by (metis not_less nth_append)
+
+lemma l_n_v_orig:
+  assumes "l0 < length env"
+  and "t \<le> l0"
+  shows "(take t env @ es @ drop t env) ! (l0 + length es) = env ! l0"
+proof -
+  from assms(1, 2) have "t < length env" by auto
+  hence h: "env = take t env @ drop t env" 
+           "length (take t env) = t"
+    apply (metis append_take_drop_id)
+    by (smt `t < length env` length_take)
+  with assms(2) have eq_sts_l: "env!l0 = (drop t env)!(l0 - t)"
+    by (metis nth_app)
+  from h(2) have "length (take t env @ es) = t + length es"
+    by (metis length_append length_replicate nat_add_commute)
+  moreover from assms(2) have "t + (length es) \<le> l0 + (length es)" by auto
+  ultimately have "((take t env @ es) @ drop t env)!(l0 + length es) = 
+                          (drop t env)!(l0+ length es - (t + length es))"
+    by (smt length_replicate length_splice nth_append)
+  with eq_sts_l[symmetric, unfolded assms]
+  show ?thesis by auto
+qed
+
+lemma l_n_v:
+  assumes "l < length sts"
+  and "sts!l = v"
+  and "t \<le> l"
+  shows "(take t sts @ replicate n x @ drop t sts) ! (l + n) = v"
+proof -
+  from l_n_v_orig[OF assms(1) assms(3), of "replicate n x"]
+  and assms(2)
+  show ?thesis by auto
+qed
+
+lemma l_n_v_s:
+  assumes "l < length sts"
+  and "t \<le> l"
+  shows "(take t sts @ sts0 @ drop t sts)[l + length sts0 := v] = 
+          take t (sts[l:=v])@ sts0 @ drop t (sts[l:=v])"
+proof -
+  let ?n = "length sts0"
+  from assms(1, 2) have "t < length sts" by auto
+  hence h: "sts = take t sts @ drop t sts" 
+           "length (take t sts) = t"
+    apply (metis append_take_drop_id)
+    by (smt `t < length sts` length_take)
+  with assms(2) have eq_sts_l: "sts[l:=v] = take t sts @ drop t sts [(l - t) := v]"
+    by (smt list_update_append)
+  with h(2) have eq_take_drop_t: "take t (sts[l:=v]) = take t sts"
+                                 "drop t (sts[l:=v]) = (drop t sts)[l - t:=v]"
+    apply (metis append_eq_conv_conj)
+    by (metis append_eq_conv_conj eq_sts_l h(2))
+  from h(2) have "length (take t sts @ sts0) = t + ?n"
+    by (metis length_append length_replicate nat_add_commute)
+  moreover from assms(2) have "t + ?n \<le> l + ?n" by auto
+  ultimately have "((take t sts @ sts0) @ drop t sts)[l + ?n := v] = 
+                   (take t sts @ sts0) @ (drop t sts)[(l + ?n - (t + ?n)) := v]"
+    by (smt list_update_append replicate_nth)
+  with eq_take_drop_t
+  show ?thesis by auto
+qed
+
+lemma l_n_v_s1: 
+  assumes "l < length sts"
+      and "\<not> t \<le> l"
+  shows "(take t sts @ sts0 @ drop t sts)[l := v] =
+         take t (sts[l := v]) @ sts0 @ drop t (sts[l := v])"
+proof(cases "t < length sts")
+  case False
+  hence h: "take t sts = sts" "drop t sts = []"
+           "take t (sts[l:=v]) = sts [l:=v]"
+           "drop t (sts[l:=v]) = []"
+    by auto
+  with assms(1)
+  show ?thesis 
+    by (metis list_update_append)
+next
+  case True
+  with assms(2)
+  have h: "(take t sts)[l:=v] = take t (sts[l:=v])"
+          "(sts[l:=v]) = (take t sts)[l:=v]@drop t sts"
+          "length (take t sts) = t"
+    apply (smt length_list_update length_take nth_equalityI nth_list_update nth_take)
+    apply (smt True append_take_drop_id assms(2) length_take list_update_append1)
+    by (smt True length_take)
+  from h(2,3) have "drop t (sts[l := v]) = drop t sts"
+    by (metis append_eq_conv_conj length_list_update)
+  with h(1)
+  show ?thesis
+    apply simp
+    by (metis assms(2) h(3) list_update_append1 not_leE)
+qed
+
+lemma l_n_v_s2:
+  assumes "l0 < length env"
+  and "t \<le> l0"
+  and "\<not> t \<le> l1"
+  shows "(take t env @ es @ drop t env) ! l1 = env ! l1"
+proof -
+  from assms(1, 2) have "t < length env" by auto
+  hence  h: "env = take t env @ drop t env" 
+            "length (take t env) = t"
+    apply (metis append_take_drop_id)
+    by (smt `t < length env` length_take)
+  with assms(3) show ?thesis
+    by (smt nth_append)
+qed
+
+lemma l_n_v_s3:
+  assumes "l0 < length env"
+  and "\<not> t \<le> l0"
+  shows "(take t env @ es @ drop t env) ! l0 = env ! l0"
+proof(cases "t < length env")
+  case True
+   hence  h: "env = take t env @ drop t env" 
+            "length (take t env) = t"
+    apply (metis append_take_drop_id)
+    by (smt `t < length env` length_take)
+  with assms(2)  show ?thesis
+    by (smt nth_append)
+next
+  case False
+  hence "take t env = env" by auto
+  with assms(1) show ?thesis
+    by (metis nth_append)
+qed
+
+subsection {* Invariant under lifts and perms *}
+
+definition "lift_b t i j = (if (j \<ge> t) then (j + i) else j)"
+
+fun lift_t :: "nat \<Rightarrow> nat \<Rightarrow> cpg \<Rightarrow> cpg"
+where "lift_t t i (CInstr ((act0, l0), (act1, l1))) = 
+                           (CInstr ((act0, lift_b t i (nat_of l0)), 
+                                    (act1, lift_b t i (nat_of l1))))" |
+      "lift_t t i (CLabel l) = CLabel (lift_b t i l)" |
+      "lift_t t i (CSeq c1 c2) = CSeq (lift_t t i c1) (lift_t t i c2)" |
+      "lift_t t i (CLocal c) = CLocal (lift_t (t + 1) i c)"
+
+definition "lift0 (i::nat) cpg = lift_t 0 i cpg"
+
+definition "perm_b t i j k = (if ((k::nat) = i \<and> i < t \<and> j < t) then j else 
+                              if (k = j \<and> i < t \<and> j < t) then i else k)"
+
+fun perm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> cpg \<Rightarrow> cpg"
+where "perm t i j (CInstr ((act0, l0), (act1, l1))) = 
+                           (CInstr ((act0, perm_b t i j l0), (act1, perm_b t i j l1)))" |
+      "perm t i j (CLabel l) = CLabel (perm_b t i j l)" |
+      "perm t i j (CSeq c1 c2) = CSeq (perm t i j c1) (perm t i j c2)" |
+      "perm t i j (CLocal c) = CLocal (perm (t + 1) (i + 1) (j + 1) c)"
+
+definition "map_idx f sts = map (\<lambda> k. sts!(f (nat k))) [0 .. int (length sts) - 1]"
+
+definition "perm_s i j sts = map_idx (perm_b (length sts) i j) sts" 
+
+fun lift_es :: "(tstate list \<times> nat) list \<Rightarrow> tstate list \<Rightarrow> tstate list" where
+    "lift_es [] env = env"
+  | "lift_es ((env', t)#ops) env = lift_es ops (take t env @ env' @ drop t env)"
+
+fun lift_ss :: "(tstate list \<times> nat) list \<Rightarrow> status list \<Rightarrow> status list" where
+    "lift_ss [] sts = sts"
+  | "lift_ss ((env', t)#ops) sts = lift_ss ops (take t sts @ map (\<lambda> x. Free) env' @ drop t sts)"
+
+
+fun lift_ts :: "(nat \<times> nat) list \<Rightarrow> cpg \<Rightarrow> cpg" where
+    "lift_ts [] cpg = cpg"
+  | "lift_ts ((lenv, t)#ops) cpg = lift_ts ops (lift_t t lenv cpg)"
+
+fun perm_ss :: "(nat \<times> nat) list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+   "perm_ss [] env = env"
+ | "perm_ss ((i, j)#ops) env = perm_ss ops (perm_s i j env)"
+
+fun perms :: "nat => (nat \<times> nat) list \<Rightarrow> cpg \<Rightarrow> cpg" where
+   "perms n [] cpg = cpg"
+ | "perms n ((i, j)#ops) cpg = perms n ops (perm n i j cpg)"
+
+definition 
+ "adjust_cpg len sps lfs cpg =  lift_ts lfs (perms len sps cpg)"
+
+definition 
+  "red_lfs lfs = map (apfst length) lfs"
+
+definition 
+ "adjust_env sps lfs env = lift_es lfs (perm_ss sps env)"
+
+definition 
+ "adjust_sts sps lfs sts = lift_ss lfs (perm_ss sps sts)"
+
+fun sts_disj_test :: "status list \<Rightarrow> status list \<Rightarrow> bool" where
+     "sts_disj_test [] [] = True" 
+  | "sts_disj_test [] (s#ss) = False"
+  | "sts_disj_test (s#ss) [] = False"
+  | "sts_disj_test (s1#ss1) (s2#ss2) = (case (s1, s2) of
+                                         (Bound, Bound) \<Rightarrow> False
+                                       | _ \<Rightarrow> sts_disj_test ss1 ss2)"
+
+lemma inj_perm_b: "inj (perm_b t i j)"
+proof(induct rule:injI)
+  case (1 x y)
+  thus ?case
+    by (unfold perm_b_def, auto split:if_splits)
+qed
+
+lemma lift_wf_cpg_test:
+  assumes "wf_cpg_test sts cpg = (True, sts')"
+  shows "wf_cpg_test (take t sts @ sts0 @ drop t sts) (lift_t t (length sts0) cpg) = 
+               (True, take t sts' @ sts0 @ drop t sts')"
+  using assms
+proof(induct cpg arbitrary:t sts0 sts sts')
+  case (CInstr instr t sts0 sts sts')
+  obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, St l0), (a1, St l1))"
+    by (metis surj_pair tstate.exhaust) 
+  from CInstr
+  show ?case
+    by (auto simp:eq_instr lift_b_def)
+next
+  case (CLabel l t sts0 sts sts')
+  thus ?case
+    apply (auto simp:lift_b_def
+                   replicate_nth replicate_update l_n_v_orig l_n_v_s)
+    apply (metis (mono_tags) diff_diff_cancel length_drop length_rev 
+             linear not_less nth_append nth_take rev_take take_all)
+    by (simp add:l_n_v_s1)
+next
+  case (CSeq c1 c2 sts0 sts sts')
+  thus ?case
+    by (auto simp: lift0_def lift_b_def split:prod.splits)
+next
+  case (CLocal body t sts0 sts sts')
+  from this(2) obtain sts1 where h: "wf_cpg_test (Free # sts) body = (True, sts1)" "tl sts1 = sts'"
+    by (auto simp:lift0_def lift_b_def split:prod.splits)
+  let ?lift_s = "\<lambda> t sts. take t sts @ sts0 @ drop t sts"
+  have eq_lift_1: "(?lift_s (Suc t) (Free # sts)) = Free#?lift_s t  sts"
+    by (simp)
+  from wf_cpg_test_le[OF h(1)] have "length (Free#sts) = length sts1"
+    by (unfold less_eq_list_def, simp)
+  hence eq_sts1: "sts1 = hd sts1 # tl sts1"
+    by (metis append_Nil append_eq_conv_conj hd.simps list.exhaust tl.simps(2))
+  from CLocal(1)[OF h(1), of "Suc t", of "sts0", unfolded eq_lift_1]
+  show ?case
+    apply (simp, subst eq_sts1, simp)
+    apply (simp add:h(2))
+    by (subst eq_sts1, simp add:h(2))
+qed
+
+lemma lift_c2t:
+  assumes "wf_cpg_test sts cpg = (True, sts')"
+  and "length env = length sts"
+  shows "c2t (take t env @ es @ drop t env) (lift_t t (length es) cpg) = 
+         c2t env cpg"
+  using assms
+proof(induct cpg arbitrary: t env es sts sts')
+  case (CInstr instr t env es sts sts')
+  obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, St l0), (a1, St l1))"
+    by (metis nat_of.cases surj_pair)
+  from CInstr have h: "l0 < length env" "l1 < length env"
+    by (auto simp:eq_instr)
+  with CInstr(2)
+  show ?case
+    by (auto simp:eq_instr lift_b_def l_n_v_orig l_n_v_s2 l_n_v_s3)
+next
+  case (CLabel l t env es sts sts')
+  thus ?case
+    by (auto simp:lift_b_def
+                replicate_nth replicate_update l_n_v_orig l_n_v_s3)
+next
+  case (CSeq c1 c2 t env es sts sts')
+  from CSeq(3) obtain sts1
+    where h: "wf_cpg_test sts c1 = (True, sts1)" "wf_cpg_test sts1 c2 = (True, sts')"
+    by (auto split:prod.splits)
+  from wf_cpg_test_le[OF h(1)] have "length sts = length sts1"
+    by (auto simp:less_eq_list_def)
+  from CSeq(4)[unfolded this] have eq_len_env: "length env = length sts1" .
+  from CSeq(1)[OF h(1) CSeq(4)]
+       CSeq(2)[OF h(2) eq_len_env]
+  show ?case
+    by (auto simp: lift0_def lift_b_def split:prod.splits)
+next
+  case (CLocal body t env es sts sts')
+  { fix x
+    from CLocal(2)
+    obtain sts1 where h1: "wf_cpg_test (Free # sts) body = (True, sts1)"
+      by (auto split:prod.splits)
+    from CLocal(3) have "length (x#env) = length (Free # sts)" by simp
+    from CLocal(1)[OF h1 this, of "Suc t"]
+    have "c2t (x # take t env @ es @ drop t env) (lift_t (Suc t) (length es) body) =
+          c2t (x # env) body"
+      by simp
+  } thus ?case by simp
+qed
+
+lemma upto_len: "length [i .. j] = (if j < i then 0 else (nat (j - i + 1)))"
+proof(induct i j rule:upto.induct)
+  case (1 i j)
+  show ?case
+  proof(cases "j < i")
+    case True
+    thus ?thesis by simp
+  next
+    case False
+    hence eq_ij: "[i..j] = i # [i + 1..j]" by (simp add:upto.simps)
+    from 1 False
+    show ?thesis
+      by (auto simp:eq_ij)
+  qed
+qed
+
+lemma upto_append:
+  assumes "x \<le> y + 1"
+  shows  "[x .. y + 1] = [x .. y]@[y + 1]"
+  using assms
+  by (induct x y rule:upto.induct, auto simp:upto.simps)
+
+lemma nth_upto:
+  assumes "l < length sts"
+  shows "[0..(int (length sts)) - 1]!l = int l"
+  using assms
+proof(induct sts arbitrary:l)
+  case Nil
+  thus ?case by simp
+next
+  case (Cons s sts l)
+  from Cons(2)
+  have "0 \<le> (int (length sts) - 1) + 1" by auto
+  from upto_append[OF this]
+  have eq_upto: "[0..int (length sts)] = [0..int (length sts) - 1] @ [int (length sts)]"
+    by simp
+  show ?case
+  proof(cases "l < length sts")
+    case True
+    with Cons(1)[OF True] eq_upto
+    show ?thesis
+      apply simp
+      by (smt nth_append take_eq_Nil upto_len)
+  next
+    case False
+    with Cons(2) have eq_l: "l = length sts" by simp
+    show ?thesis
+    proof(cases sts)
+      case (Cons x xs)
+      have "[0..1 + int (length xs)] = [0 .. int (length xs)]@[1 + int (length xs)]"
+        by (smt upto_append)
+      moreover have "length [0 .. int (length xs)] = Suc (length xs)"
+        by (smt upto_len)
+      moreover note Cons
+      ultimately show ?thesis
+        apply (simp add:eq_l)
+        by (smt nth_Cons' nth_append)
+    qed (simp add:upto_len upto.simps eq_l)
+  qed
+qed
+
+lemma map_idx_idx: 
+  assumes "l < length sts"
+  shows "(map_idx f sts)!l = sts!(f l)"
+proof -
+  from assms have lt_l: "l < length [0..int (length sts) - 1]"
+    by (smt upto_len)
+  show ?thesis
+    apply (unfold map_idx_def nth_map[OF lt_l])
+    by (metis assms nat_int nth_upto)
+qed
+
+lemma map_idx_len: "length (map_idx f sts) = length sts"
+  apply (unfold map_idx_def)
+  by (smt length_map upto_len)
+  
+lemma map_idx_eq:
+  assumes "\<forall> l < length sts. f l = g l"
+  shows "map_idx f sts = map_idx g sts"
+proof(induct rule: nth_equalityI)
+  case 1
+  show "length (map_idx f sts) = length (map_idx g sts)"
+    by (metis map_idx_len)
+next
+  case 2
+  { fix l
+    assume "l < length (map_idx f sts)"
+    hence "l < length sts"
+      by (metis map_idx_len)
+    from map_idx_idx[OF this] and assms and this
+    have "map_idx f sts ! l = map_idx g sts ! l"
+      by (smt list_eq_iff_nth_eq map_idx_idx map_idx_len)
+  } thus ?case by auto
+qed
+
+lemma perm_s_commut: "perm_s i j sts = perm_s j i sts"
+  apply (unfold perm_s_def, rule map_idx_eq, unfold perm_b_def)
+  by smt
+
+lemma map_idx_id: "map_idx id sts = sts"
+proof(induct rule:nth_equalityI)
+  case 1
+  from map_idx_len show "length (map_idx id sts) = length sts" .
+next
+  case 2
+  { fix l
+    assume "l < length (map_idx id sts)"
+    from map_idx_idx[OF this[unfolded map_idx_len]]
+    have "map_idx id sts ! l = sts ! l" by simp
+  } thus ?case by auto
+qed
+
+lemma perm_s_lt_i: 
+  assumes "\<not> i < length sts"
+  shows "perm_s i j sts = sts"
+proof -
+  have "map_idx (perm_b (length sts) i j) sts = map_idx id sts" 
+  proof(rule map_idx_eq, default, clarsimp)
+    fix l
+    assume "l < length sts"
+    with assms
+    show "perm_b (length sts) i j l = l"
+      by (unfold perm_b_def, auto)
+  qed
+  with map_idx_id
+  have "map_idx (perm_b (length sts) i j) sts = sts" by simp
+  thus ?thesis by (simp add:perm_s_def)
+qed
+
+lemma perm_s_lt:
+  assumes "\<not> i < length sts \<or> \<not> j < length sts"
+  shows "perm_s i j sts = sts"
+  using assms
+proof
+  assume "\<not> i < length sts"
+  from perm_s_lt_i[OF this] show ?thesis .
+next
+  assume "\<not> j < length sts"
+  from perm_s_lt_i[OF this, of i, unfolded perm_s_commut]
+  show ?thesis .
+qed
+
+lemma perm_s_update_i:
+  assumes "i < length sts" 
+  and "j < length sts"
+  shows "sts ! i = perm_s i j sts ! j"
+proof -
+  from map_idx_idx[OF assms(2)]
+  have "map_idx (perm_b (length sts) i j) sts ! j = sts!(perm_b (length sts) i j j)" .
+  with assms
+  show ?thesis 
+    by (auto simp:perm_s_def perm_b_def)
+qed
+
+lemma nth_perm_s_neq:
+  assumes "l \<noteq> j"
+  and "l \<noteq> i"
+  and "l < length sts"
+  shows "sts ! l = perm_s i j sts ! l"
+proof -
+  have "map_idx (perm_b (length sts) i j) sts ! l = sts!(perm_b (length sts) i j l)"
+    by (metis assms(3) map_idx_def map_idx_idx)
+  with assms
+  show ?thesis
+    by (unfold perm_s_def perm_b_def, auto)
+qed
+
+lemma map_idx_update:
+  assumes "f j = i"
+  and "inj f"
+  and "i < length sts"
+  and "j < length sts"
+  shows "map_idx f (sts[i:=v]) = map_idx f sts[j := v]"
+proof(induct rule:nth_equalityI)
+  case 1
+  show "length (map_idx f (sts[i := v])) = length (map_idx f sts[j := v])"
+    by (metis length_list_update map_idx_len)
+next
+  case 2
+  { fix l
+    assume lt_l: "l < length (map_idx f (sts[i := v]))"
+    have eq_nth: "sts[i := v] ! f l = map_idx f sts[j := v] ! l"
+    proof(cases "f l = i")
+      case False
+      from lt_l have "l < length sts"
+        by (metis length_list_update map_idx_len)
+      from map_idx_idx[OF this, of f] have " map_idx f sts ! l = sts ! f l" .
+      moreover from False assms have "l \<noteq> j" by auto
+      moreover note False
+      ultimately show ?thesis by simp
+    next
+      case True
+      with assms have eq_l: "l = j" 
+        by (metis inj_eq)
+      moreover from lt_l eq_l 
+      have "j < length (map_idx f sts[j := v])"
+        by (metis length_list_update map_idx_len)
+      moreover note True assms
+      ultimately show ?thesis by simp
+    qed
+    from lt_l have "l < length (sts[i := v])"
+      by (metis map_idx_len)
+    from map_idx_idx[OF this] eq_nth
+    have "map_idx f (sts[i := v]) ! l = map_idx f sts[j := v] ! l" by simp
+  } thus ?case by auto
+qed
+
+lemma perm_s_update:
+  assumes "i < length sts"
+  and "j < length sts"
+  shows "(perm_s i j sts)[i := v] = perm_s i j (sts[j := v])"
+proof -
+  have "map_idx (perm_b (length (sts[j := v])) i j) (sts[j := v]) = 
+        map_idx (perm_b (length (sts[j := v])) i j) sts[i := v]"
+    proof(rule  map_idx_update[OF _ _ assms(2, 1)])
+      from inj_perm_b show "inj (perm_b (length (sts[j := v])) i j)" .
+    next
+      from assms show "perm_b (length (sts[j := v])) i j i = j"
+        by (auto simp:perm_b_def)
+    qed
+  hence "map_idx (perm_b (length sts) i j) sts[i := v] =
+        map_idx (perm_b (length (sts[j := v])) i j) (sts[j := v])"
+    by simp
+  thus ?thesis by (simp add:perm_s_def)
+qed
+
+lemma perm_s_len: "length (perm_s i j sts') = length sts'"
+  apply (unfold perm_s_def map_idx_def)
+  by (smt Nil_is_map_conv length_0_conv length_greater_0_conv length_map neq_if_length_neq upto_len)
+
+lemma perm_s_update_neq:
+  assumes "l \<noteq> i"
+  and "l \<noteq> j"
+  shows "perm_s i j sts[l := v] = perm_s i j (sts[l := v])"
+proof(cases "i < length sts \<and> j < length sts")
+  case False
+  with perm_s_lt have "perm_s i j sts = sts" by auto
+  moreover have "perm_s i j (sts[l:=v]) = sts[l:=v]"
+  proof -
+    have "length (sts[l:=v]) = length sts" by auto
+    from False[folded this] perm_s_lt
+    show ?thesis by metis
+  qed
+  ultimately show ?thesis by simp
+next
+  case True
+  note lt_ij = this
+  show ?thesis
+  proof(cases "l < length sts")
+    case False
+    hence "sts[l:=v] = sts" by auto
+    moreover have "perm_s i j sts[l := v] = perm_s i j sts"
+    proof -
+      from False and perm_s_len
+      have "\<not> l < length (perm_s i j sts)" by metis
+      thus ?thesis by auto
+    qed
+    ultimately show ?thesis by simp
+  next
+    case True
+    show ?thesis
+    proof -
+      have "map_idx (perm_b (length (sts[l := v])) i j) (sts[l := v]) = 
+            map_idx (perm_b (length (sts[l := v])) i j) sts[l := v]"
+      proof(induct rule:map_idx_update [OF _ inj_perm_b True True])
+        case 1
+        from assms lt_ij
+        show ?case
+          by (unfold perm_b_def, auto)
+      qed
+      thus ?thesis
+        by (unfold perm_s_def, simp)
+    qed
+  qed
+qed
+
+lemma perm_sb: "(perm_s i j sts)[perm_b (length sts) i j l := v] = perm_s i j (sts[l := v])"
+  apply(subst perm_b_def, auto simp:perm_s_len perm_s_lt perm_s_update)
+  apply (subst perm_s_commut, subst (2) perm_s_commut, rule_tac perm_s_update, auto)
+  by (rule_tac perm_s_update_neq, auto)
+
+lemma perm_s_id: "perm_s i i sts = sts" (is "?L = ?R")
+proof -
+  from map_idx_id have "?R = map_idx id sts" by metis
+  also have "\<dots> = ?L"
+    by (unfold perm_s_def, rule map_idx_eq, unfold perm_b_def, auto)
+  finally show ?thesis by simp
+qed
+
+lemma upto_map:
+  assumes "i \<le> j"
+  shows "[i .. j] = i # map (\<lambda> x. x + 1) [i .. (j - 1)]"
+  using assms
+proof(induct i j rule:upto.induct)
+  case (1 i j)
+  show ?case (is "?L = ?R")
+  proof -
+    from 1(2)
+    have eq_l: "?L = i # [i+1 .. j]" by (simp add:upto.simps)
+    show ?thesis
+    proof(cases "i + 1 \<le> j")
+      case False
+      with eq_l show ?thesis by (auto simp:upto.simps)
+    next
+      case True
+      have "[i + 1..j] =  map (\<lambda>x. x + 1) [i..j - 1]"
+        by (smt "1.hyps" Cons_eq_map_conv True upto.simps)
+      with eq_l
+      show ?thesis by simp
+    qed
+  qed
+qed
+
+lemma perm_s_cons: "(perm_s (Suc i) (Suc j) (s # sts)) = s#perm_s i j sts"
+proof -
+  have le_0: "0 \<le> int (length (s # sts)) - 1" by simp
+  have "map (\<lambda>k. (s # sts) ! perm_b (length (s # sts)) (Suc i) (Suc j) (nat k))
+          [0..int (length (s # sts)) - 1] =
+                 s # map (\<lambda>k. sts ! perm_b (length sts) i j (nat k)) [0..int (length sts) - 1]"
+    by (unfold upto_map[OF le_0], auto simp:perm_b_def, smt+)
+  thus ?thesis by (unfold perm_s_def map_idx_def, simp)
+qed
+
+lemma perm_wf_cpg_test:
+  assumes "wf_cpg_test sts cpg = (True, sts')"
+  shows "wf_cpg_test (perm_s i j sts) (perm (length sts) i j cpg) = 
+               (True, perm_s i j sts')"
+  using assms
+proof(induct cpg arbitrary:t i j sts sts')
+  case (CInstr instr i j sts sts')
+  obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, St l0), (a1, St l1))"
+    by (metis surj_pair tstate.exhaust)
+  from CInstr
+  show ?case
+    apply (unfold eq_instr, clarsimp)
+    by (unfold perm_s_len perm_b_def, clarsimp)
+next
+  case (CLabel l i j sts sts')
+  have "(perm_s i j sts)[perm_b (length sts) i j l := Bound] = perm_s i j (sts[l := Bound])"
+    by (metis perm_sb)
+  with CLabel
+  show ?case
+    apply (auto simp:perm_s_len perm_sb)
+    apply (subst perm_b_def, auto simp:perm_sb)
+    apply (subst perm_b_def, auto simp:perm_s_lt perm_s_update_i)
+    apply (unfold perm_s_id, subst perm_s_commut, simp add: perm_s_update_i[symmetric])
+    apply (simp add:perm_s_update_i[symmetric])
+    by (simp add: nth_perm_s_neq[symmetric])
+next
+  case (CSeq c1 c2 i j sts sts')
+  thus ?case
+    apply (auto  split:prod.splits)
+    apply (metis (hide_lams, no_types) less_eq_list_def prod.inject wf_cpg_test_le)
+    by (metis (hide_lams, no_types) less_eq_list_def prod.inject wf_cpg_test_le)
+next
+  case (CLocal body i j sts sts')
+  from this(2) obtain sts1 where h: "wf_cpg_test (Free # sts) body = (True, sts1)" "tl sts1 = sts'"
+    by (auto simp:lift0_def lift_b_def split:prod.splits)
+  from wf_cpg_test_le[OF h(1)] have "length (Free#sts) = length sts1"
+    by (unfold less_eq_list_def, simp)
+  hence eq_sts1: "sts1 = hd sts1 # tl sts1"
+    by (metis append_Nil append_eq_conv_conj hd.simps list.exhaust tl.simps(2))
+  from CLocal(1)[OF h(1), of "Suc i" "Suc j"] h(2) eq_sts1
+  show ?case
+    apply (auto split:prod.splits simp:perm_s_cons)
+    by (metis perm_s_cons tl.simps(2))
+qed
+
+lemma nth_perm_sb:
+  assumes "l0 < length env"
+  shows "perm_s i j env ! perm_b (length env) i j l0 = env ! l0"
+  by (metis assms nth_perm_s_neq perm_b_def perm_s_commut perm_s_lt perm_s_update_i)
+  
+
+lemma perm_c2t:  
+  assumes "wf_cpg_test sts cpg = (True, sts')"
+  and "length env = length sts"
+  shows "c2t  (perm_s i j env) (perm (length env) i j cpg)  = 
+         c2t env cpg"
+  using assms
+proof(induct cpg arbitrary:i j env sts sts')
+  case (CInstr instr i j env sts sts')
+  obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, St l0), (a1, St l1))"
+    by (metis surj_pair tstate.exhaust) 
+  from CInstr have h: "l0 < length env" "l1 < length env"
+    by (auto simp:eq_instr)
+  with CInstr(2)
+  show ?case
+    apply (auto simp:eq_instr)
+    by (metis nth_perm_sb)+
+next
+  case (CLabel l t env es sts sts')
+  thus ?case
+    apply (auto)
+    by (metis nth_perm_sb)
+next
+  case (CSeq c1 c2 i j env sts sts')
+  from CSeq(3) obtain sts1
+    where h: "wf_cpg_test sts c1 = (True, sts1)" "wf_cpg_test sts1 c2 = (True, sts')"
+    by (auto split:prod.splits)
+  from wf_cpg_test_le[OF h(1)] have "length sts = length sts1"
+    by (auto simp:less_eq_list_def)
+  from CSeq(4)[unfolded this] have eq_len_env: "length env = length sts1" .
+  from CSeq(1)[OF h(1) CSeq(4)]
+       CSeq(2)[OF h(2) eq_len_env]
+  show ?case by auto
+next
+  case (CLocal body i j env sts sts')
+  { fix x
+    from CLocal(2, 3)
+    obtain sts1 where "wf_cpg_test (Free # sts) body = (True, sts1)"
+                      "length (x#env) = length (Free # sts)"
+      by (auto split:prod.splits)
+    from CLocal(1)[OF this]
+    have "(c2t (x # perm_s i j env) (perm (Suc (length env)) (Suc i) (Suc j) body)) =
+                 (c2t (x # env) body)"
+      by (metis Suc_length_conv perm_s_cons)
+  } thus ?case by simp
+qed
+
+lemma wf_cpg_test_disj_aux1:
+  assumes "sts_disj sts1 (sts[l := Bound] - sts)"
+              "l < length sts"
+              "sts ! l = Free"
+  shows "(sts1 + sts) ! l = Free"
+proof -
+  from assms(1)[unfolded sts_disj_def]
+  have h: "length sts1 = length (sts[l := Bound] - sts)"
+          "(\<forall>i<length sts1. \<not> (sts1 ! i = Bound \<and> (sts[l := Bound] - sts) ! i = Bound))"
+    by auto
+  from h(1) assms(2) 
+  have lt_l: "l < length sts1" 
+             "l < length (sts[l := Bound] - sts)"
+             "l < length (sts1 + sts)"
+    apply (smt length_list_update minus_list_len)
+    apply (smt assms(2) length_list_update minus_list_len)
+    by (smt assms(2) h(1) length_list_update length_sts_plus minus_list_len)
+  from h(2)[rule_format, of l, OF this(1)] 
+  have " \<not> (sts1 ! l = Bound \<and> (sts[l := Bound] - sts) ! l = Bound)" .
+  with assms(3) nth_sts_minus[OF lt_l(2)] nth_sts_plus[OF lt_l(3)] assms(2)
+  show ?thesis
+    by (cases "sts1!l", auto)
+qed
+
+lemma  wf_cpg_test_disj_aux2: 
+  assumes "sts_disj sts1 (sts[l := Bound] - sts)"
+          " l < length sts"
+  shows "(sts1 + sts)[l := Bound] = sts1 + sts[l := Bound]"
+proof -
+ from assms have lt_l: "l < length (sts1 + sts[l:=Bound])"
+                       "l < length (sts1 + sts)"
+   apply (smt length_list_update length_sts_plus minus_list_len sts_disj_def)
+   by (smt assms(1) assms(2) length_list_update length_sts_plus minus_list_len sts_disj_def)
+ show ?thesis
+ proof(induct rule:nth_equalityI)
+   case 1
+   show ?case
+     by (smt assms(1) length_list_update length_sts_plus minus_list_len sts_disj_def)
+ next
+   case 2
+   { fix i 
+     assume lt_i: "i < length ((sts1 + sts)[l := Bound])"
+     have " (sts1 + sts)[l := Bound] ! i = (sts1 + sts[l := Bound]) ! i"
+     proof(cases "i = l")
+       case True
+       with nth_sts_plus[OF lt_l(1)] assms(2) nth_sts_plus[OF lt_l(2)] lt_l
+       show ?thesis
+         by (cases "sts1 ! l", auto)
+     next
+       case False
+       from lt_i have "i < length (sts1 + sts)" "i < length (sts1 + sts[l := Bound])"
+         apply auto
+         by (metis length_list_update plus_list_len)
+       from nth_sts_plus[OF this(1)] nth_sts_plus[OF this(2)] lt_i lt_l False
+       show ?thesis
+         by simp
+     qed
+   } thus ?case by auto
+ qed
+qed
+
+lemma sts_list_plus_commut:
+  shows "sts1 + sts2 = sts2 + (sts1:: status list)"
+proof(induct rule:nth_equalityI)
+  case 1
+  show ?case
+    by (metis min_max.inf.commute plus_list_len)
+next
+  case 2
+  { fix i
+    assume lt_i1: "i<length (sts1 + sts2)"
+    hence lt_i2: "i < length (sts2 + sts1)"
+      by (smt plus_list_len)
+    from nth_sts_plus[OF this] nth_sts_plus[OF lt_i1]
+    have "(sts1 + sts2) ! i = (sts2 + sts1) ! i"
+      apply simp
+      apply (cases "sts1!i", cases "sts2!i", auto)
+      by (cases "sts2!i", auto)
+  } thus ?case by auto
+qed
+
+lemma sts_disj_cons:
+  assumes "sts_disj sts1 sts2"
+  shows "sts_disj (Free # sts1) (s # sts2)"
+  using assms
+proof -
+  from assms 
+  have h: "length sts1 = length sts2"
+          "(\<forall>i<length sts1. \<not> (sts1 ! i = Bound \<and> sts2 ! i = Bound))"
+    by (unfold sts_disj_def, auto)
+  from h(1) have "length (Free # sts1) = length (s # sts2)" by simp
+  moreover {
+    fix i
+    assume lt_i: "i<length (Free # sts1)"
+    have "\<not> ((Free # sts1) ! i = Bound \<and> (s # sts2) ! i = Bound)"
+    proof(cases "i")
+      case 0
+      thus ?thesis by simp
+    next
+      case (Suc k)
+      from h(2)[rule_format, of k] lt_i[unfolded Suc] Suc
+      show ?thesis by auto
+    qed
+  }
+  ultimately show ?thesis by (auto simp:sts_disj_def)
+qed
+
+lemma sts_disj_uncomb:
+  assumes "sts_disj sts (sts1 + sts2)"
+  and "sts_disj sts1 sts2"
+  shows "sts_disj sts sts1" "sts_disj sts sts2"
+  using assms
+  apply  (smt assms(1) assms(2) length_sts_plus nth_sts_plus plus_status.simps(2) sts_disj_def)
+  by (smt assms(1) assms(2) length_sts_plus nth_sts_plus 
+       plus_status.simps(2) sts_disj_def sts_list_plus_commut)
+
+lemma wf_cpg_test_disj:
+  assumes "wf_cpg_test sts cpg = (True, sts')"
+  and "sts_disj sts1 (sts' - sts)"
+  shows "wf_cpg_test (sts1 + sts) cpg = (True, sts1 + sts')"
+  using assms
+proof(induct cpg arbitrary:sts sts1 sts')
+  case (CInstr instr sts sts1 sts')
+  obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, St l0), (a1, St l1))"
+    by (metis nat_of.cases surj_pair)
+  with CInstr(1) have h: "l0 < length sts" "l1 < length sts" "sts = sts'" by auto
+  with CInstr eq_instr
+  show ?case
+    apply (auto)
+    by (smt length_sts_plus minus_list_len sts_disj_def)+
+next
+  case (CLabel l sts sts1 sts')
+  thus ?case
+    apply auto
+    apply (smt length_list_update length_sts_plus minus_list_len sts_disj_def)
+    by (auto simp: wf_cpg_test_disj_aux1 wf_cpg_test_disj_aux2)
+next
+  case (CSeq c1 c2 sts sts1 sts')
+  from CSeq(3) obtain sts''
+    where h: "wf_cpg_test sts c1 = (True, sts'')" "wf_cpg_test sts'' c2 = (True, sts')"
+    by (auto split:prod.splits)
+  from wf_cpg_test_le[OF h(1)] have "length sts = length sts''"
+    by (auto simp:less_eq_list_def)
+  from sts_le_comb[OF wf_cpg_test_le[OF h(1)] wf_cpg_test_le[OF h(2)]]
+  have " sts' - sts = (sts'' - sts) + (sts' - sts'')" "sts_disj (sts'' - sts) (sts' - sts'')"
+    by auto
+  from sts_disj_uncomb[OF CSeq(4)[unfolded this(1)] this(2)]
+  have "sts_disj sts1 (sts'' - sts)" "sts_disj sts1 (sts' - sts'')" .
+  from CSeq(1)[OF h(1) this(1)] CSeq(2)[OF h(2) this(2)]
+  have "wf_cpg_test (sts1 + sts) c1 = (True, sts1 + sts'')"
+       "wf_cpg_test (sts1 + sts'') c2 = (True, sts1 + sts')" .
+  thus ?case
+    by simp
+next
+  case (CLocal body sts sts1 sts')
+  from this(2)
+  obtain sts'' where h: "wf_cpg_test (Free # sts) body = (True, sts'')" "sts' = tl sts''"
+    by (auto split:prod.splits)
+  from wf_cpg_test_le[OF h(1), unfolded less_eq_list_def] h(2)
+  obtain s where eq_sts'': "sts'' = s#sts'"
+    by (metis Suc_length_conv list.size(4) tl.simps(2))
+  let ?sts = "Free#sts1"
+  from CLocal(3) have "sts_disj ?sts (sts'' - (Free # sts))"
+    apply (unfold eq_sts'', simp)
+    by (metis sts_disj_cons)
+  from CLocal(1)[OF h(1) this] eq_sts''
+  show ?case
+    by (auto split:prod.splits)
+qed
+
+lemma sts_disj_free:
+  assumes "list_all (op = Free) sts"
+     and "length sts' = length sts"
+  shows "sts_disj sts' sts"
+by (metis (full_types) assms(1) assms(2) list_all_length 
+     status.distinct(1) sts_disj_def)
+
+lemma all_free_plus:
+  assumes "length sts' = length sts"
+  and "list_all (op = Free) sts"
+  shows "sts' + sts = sts'"
+  using assms
+proof(induct sts' arbitrary:sts)
+  case (Cons s sts' sts)
+  note cs = Cons
+  thus ?case
+  proof(cases "sts")
+    case (Cons s1 sts1)
+    with cs
+    show ?thesis
+      by (smt list.size(4) list_all_simps(1) 
+              plus_list.simps(3) plus_status.simps(1) sts_list_plus_commut)
+  qed auto
+qed auto
+
+lemma wf_cpg_test_extrapo:
+  assumes "wf_cpg_test sts cpg = (True, sts)"
+  and "list_all (op = Free) sts"
+  and "length sts' = length sts"
+  shows "wf_cpg_test sts' cpg = (True, sts')"
+proof -
+  have "sts_disj sts' (sts - sts)"
+  proof(rule sts_disj_free)
+    from assms(2)
+    show "list_all (op = Free) (sts - sts)"
+      by (induct sts, auto)
+  next
+    from assms(3) show "length sts' = length (sts - sts)"
+      by (metis length_sts_plus minus_list_len plus_list_len)
+  qed
+  from wf_cpg_test_disj [OF assms(1) this]
+  have "wf_cpg_test (sts' + sts) cpg = (True, sts' + sts)" .
+  moreover from all_free_plus[OF assms(3, 2)] have "sts' + sts = sts'" .
+  finally show ?thesis by simp
+qed
+
+lemma perms_wf_cpg_test:
+  assumes "wf_cpg_test sts cpg = (True, sts')"
+  shows "wf_cpg_test (perm_ss ops sts) (perms (length sts) ops cpg) = 
+                   (True, perm_ss ops sts')"
+  using assms
+proof(induct ops arbitrary:sts cpg sts')
+  case (Cons sp ops sts cpg sts')
+  show ?case
+  proof(cases "sp")
+    case (Pair i j)
+    show ?thesis
+    proof -
+      let ?sts = "(perm_s i j sts)" and ?cpg = "(perm (length sts) i j cpg)"
+      and ?sts' = "perm_s i j sts'"
+      have "wf_cpg_test (perm_ss ops ?sts) (perms (length ?sts) ops ?cpg) = 
+                     (True, perm_ss ops ?sts')"
+      proof(rule Cons(1))
+        show "wf_cpg_test (perm_s i j sts) (perm (length sts) i j cpg) = (True, perm_s i j sts')"
+          by (metis Cons.prems perm_wf_cpg_test)
+      qed
+      thus ?thesis
+        apply (unfold Pair)
+        apply simp
+        by (metis perm_s_len)
+    qed
+  qed
+qed auto
+
+lemma perm_ss_len: "length (perm_ss ops xs) = length xs"
+proof(induct ops arbitrary:xs)
+  case (Cons sp ops xs)
+  show ?case
+  proof(cases "sp")
+    case (Pair i j)
+    show ?thesis
+    proof -
+      let ?xs = "(perm_s i j xs)"
+      have "length (perm_ss ops ?xs) = length ?xs"
+        by (metis Cons.hyps)
+      also have "\<dots> = length xs"
+        by (metis perm_s_len)
+      finally show ?thesis
+        by (unfold Pair, simp)
+    qed
+  qed
+qed auto
+
+lemma perms_c2t: 
+  assumes "wf_cpg_test sts cpg = (True, sts')"
+   and "length env = length sts"
+  shows "c2t (perm_ss ops env) (perms (length env) ops cpg) = c2t env cpg"
+  using assms
+proof(induct ops arbitrary:sts cpg sts' env)
+  case (Cons sp ops sts cpg sts' env)
+  show ?case
+  proof(cases "sp")
+    case (Pair i j)
+    show ?thesis
+    proof -
+      let ?env = "(perm_s i j env)" and ?cpg = "(perm (length env) i j cpg)"
+      have " c2t (perm_ss ops ?env) (perms (length ?env) ops ?cpg) = c2t ?env ?cpg"
+      proof(rule Cons(1))
+        from perm_wf_cpg_test[OF Cons(2), of i j, folded Cons(3)]
+        show "wf_cpg_test (perm_s i j sts) (perm (length env) i j cpg) = (True, perm_s i j sts')" .
+      next
+        show "length (perm_s i j env) = length (perm_s i j sts)"
+          by (metis Cons.prems(2) perm_s_len)
+      qed
+      also have "\<dots> = c2t env cpg"
+        by (metis Cons.prems(1) Cons.prems(2) perm_c2t)
+      finally show ?thesis
+        apply (unfold Pair)
+        apply simp
+        by (metis perm_s_len)
+    qed
+  qed
+qed auto
+
+lemma red_lfs_nil: "red_lfs [] = []"
+  by (simp add:red_lfs_def)
+
+lemma red_lfs_cons: "red_lfs ((env, t)#lfs) = (length env, t)#(red_lfs lfs)"
+  by (simp add:red_lfs_def)
+
+lemmas red_lfs_simps [simp] = red_lfs_nil red_lfs_cons
+
+lemma lifts_wf_cpg_test: 
+  assumes "wf_cpg_test sts cpg = (True, sts')"
+  shows "wf_cpg_test (lift_ss ops sts) (lift_ts (red_lfs ops) cpg) 
+                =  (True, lift_ss ops sts')"
+  using assms
+proof(induct ops arbitrary:sts cpg sts')
+  case (Cons sp ops sts cpg sts')
+  show ?case
+  proof(cases "sp")
+    case (Pair env' t)
+    thus ?thesis
+    proof -
+      let ?sts = "(take t sts @ map (\<lambda>x. Free) env' @ drop t sts)" 
+      and ?sts' = "(take t sts' @ map (\<lambda>x. Free) env' @ drop t sts')"
+      and ?cpg = "(lift_t t (length env') cpg)"
+      have "wf_cpg_test (lift_ss ops ?sts) (lift_ts (red_lfs ops) ?cpg) = (True, lift_ss ops ?sts')"
+      proof(induct rule: Cons(1))
+        case 1
+        show ?case
+          by (metis Cons.prems length_map lift_wf_cpg_test)
+      qed
+      thus ?thesis
+        by (unfold Pair, simp)
+    qed
+  qed
+qed auto
+
+lemma lifts_c2t: 
+  assumes "wf_cpg_test sts cpg = (True, sts')"
+   and "length env = length sts"
+  shows "c2t (lift_es ops env) (lift_ts (red_lfs ops) cpg) = c2t env cpg"
+  using assms
+proof(induct ops arbitrary:sts cpg sts' env)
+  case (Cons sp ops sts cpg sts' env)
+  show ?case
+  proof(cases "sp")
+    case (Pair env' t)
+    show ?thesis
+    proof -
+      let ?env = "(take t env @ env' @ drop t env)" 
+      and ?cpg = "(lift_t t (length env') cpg)"
+      have "c2t (lift_es ops ?env) (lift_ts (red_lfs ops) ?cpg) = c2t ?env ?cpg"
+      proof(rule Cons(1))
+        from lift_wf_cpg_test[OF Cons(2), of t "map (\<lambda> x. Free) env'", simplified length_map]
+        show "wf_cpg_test (take t sts @ map (\<lambda>x. Free) env' @ drop t sts) 
+                  (lift_t t (length env') cpg) =
+              (True, take t sts' @ map (\<lambda>x. Free) env' @ drop t sts')" .
+      next
+        show "length (take t env @ env' @ drop t env) =
+                length (take t sts @ map (\<lambda>x. Free) env' @ drop t sts)"
+          by (metis (full_types) Cons.prems(2) Pair assms(2) length_append 
+                  length_drop length_map length_take)
+      qed
+      also have "\<dots> = c2t env cpg"
+        by (metis Cons.prems(1) Cons.prems(2) lift_c2t)
+      finally show ?thesis
+        by (unfold Pair, simp)
+    qed
+  qed
+qed auto
+
+lemma adjust_c2t: 
+  assumes "wf_cpg_test sts cpg = (True, sts')"
+  and "length env = length sts"
+  shows "c2t (adjust_env sps lfs env) (adjust_cpg (length sts) sps (red_lfs lfs) cpg) = c2t env cpg"
+proof -
+  let ?cpg = "(perms (length sts) sps cpg)"
+  and ?env = "(perm_ss sps env)"
+  have "c2t (lift_es lfs ?env) 
+               (lift_ts (red_lfs lfs) ?cpg) = c2t ?env ?cpg"
+  proof (rule lifts_c2t)
+    from perms_wf_cpg_test[OF assms(1), of sps]
+    show "wf_cpg_test (perm_ss sps sts) (perms (length sts) sps cpg) = (True, perm_ss sps sts')" .
+  next
+    show "length (perm_ss sps env) = length (perm_ss sps sts)"
+      by (metis assms(2) perm_ss_len)
+  qed
+  also have "\<dots> = c2t env cpg"
+  proof(fold assms(2), rule perms_c2t)
+    from assms(1) show " wf_cpg_test sts cpg = (True, sts')" .
+  next
+    from assms(2) show "length env = length sts" .
+  qed
+  finally show ?thesis
+    by (unfold adjust_env_def adjust_cpg_def, simp)
+qed
+
+lemma adjust_wf_cpg_test:
+  assumes "wf_cpg_test sts cpg = (True, sts')"
+  shows "wf_cpg_test (adjust_sts sps lfs sts) (adjust_cpg (length sts) sps (red_lfs lfs) cpg) = 
+                         (True, adjust_sts sps lfs sts')"
+proof -
+  have " wf_cpg_test (lift_ss lfs (perm_ss sps sts)) (lift_ts (red_lfs lfs) (perms (length sts) sps cpg)) =
+    (True, lift_ss lfs (perm_ss sps sts'))"
+  proof(rule lifts_wf_cpg_test)
+    show " wf_cpg_test (perm_ss sps sts) (perms (length sts) sps cpg) = (True, perm_ss sps sts')"
+      by (rule perms_wf_cpg_test[OF assms])
+  qed
+  thus ?thesis
+    by (unfold adjust_sts_def adjust_cpg_def, simp)
+qed
+
+lemma sts_disj_test_correct:
+  assumes "sts_disj_test sts1 sts2"
+  shows "sts_disj sts1 sts2"
+  using assms
+proof(induct sts1 arbitrary:sts2)
+  case (Nil sts2)
+  note Nil_1 = Nil
+  show ?case
+  proof(cases sts2)
+    case Nil
+    with Nil_1
+    show ?thesis by (simp add:sts_disj_def)
+  next
+    case (Cons s2 ss2)
+    with Nil_1 show ?thesis by simp
+  qed
+next
+  case (Cons s1 ss1 sts2)
+  note Cons_1 = Cons
+  show ?case
+  proof(cases "sts2")
+    case Nil
+    with Cons_1 show ?thesis by simp
+  next
+    case (Cons s2 ss2)
+    show ?thesis
+    proof(cases "s1 = Bound \<and> s2 = Bound")
+      case True
+      with Cons_1 Cons
+      show ?thesis by simp
+    next
+      case False
+      with Cons_1 Cons
+      have "sts_disj_test ss1 ss2" by (auto split:status.splits)
+      from Cons_1(1) [OF this] False
+      show ?thesis
+        apply (unfold Cons)
+        apply (unfold sts_disj_def)
+        by (smt False length_Suc_conv list.size(4) nth_Cons')
+    qed      
+  qed
+qed
+
+lemma sts_minus_free:
+  assumes "length sts1 = length sts2"
+  and "list_all (op = Free) sts2"
+  shows "sts1 - sts2 = sts1"
+  using assms
+proof(induct sts1 arbitrary:sts2)
+  case (Nil sts2)
+  thus ?case by simp
+next
+  case (Cons s1 ss1 sts2)
+  note Cons_1 = Cons
+  thus ?case
+  proof(cases sts2)
+    case Nil
+    with Cons
+    show ?thesis by simp
+  next
+    case (Cons s2 ss2)
+    have "ss1 - ss2 = ss1"
+    proof(rule Cons_1(1))
+      show "length ss1 = length ss2"
+        by (metis Cons Cons_1(2) Suc_length_conv list.inject)
+    next
+      show "list_all (op = Free) ss2"
+        by (metis Cons Cons_1(3) list_all_simps(1))
+    qed
+    moreover from Cons_1(3) Cons have "s2 = Free"
+      by (metis (full_types) list_all_simps(1))
+    ultimately show ?thesis using Cons
+      apply simp
+      by (metis (hide_lams, mono_tags) minus_status.simps(2) minus_status.simps(3) status.exhaust)
+  qed
+qed
+
+lemma st_simp [simp]: "St (nat_of x) = x"
+  by (metis nat_of.simps tstate.exhaust)
+  
+lemma wf_cpg_test_len:
+  assumes "wf_cpg_test sts cpg = (b, sts')"
+  shows "length sts' = length sts"
+  using assms
+proof(induct cpg arbitrary:sts sts' b)
+  case (CInstr instr sts sts' b)
+  then obtain a1 s1 a2 s2 where
+    eq_instr: "instr = ((a1, St s1), (a2, St s2))"
+    by (metis st_simp surj_pair) 
+  with CInstr
+  show ?case by simp
+qed (auto split:prod.splits)
+
+lemma wf_cpg_test_seq:
+  assumes "wf_cpg_test sts1 c1 = (True, sts1')"
+  and "wf_cpg_test sts2 c2 = (True, sts2')"
+  and "length sts1 = length sts2"
+  and "list_all (op = Free) sts1"
+  and "list_all (op = Free) sts2"
+  and "sts_disj_test sts1' sts2'"
+  shows "wf_cpg_test sts1 (CSeq c1 c2) = (True, sts1' + sts2')"
+proof -
+  have "wf_cpg_test (sts1' + sts2) c2 = (True, sts1' + sts2')"
+    by (metis add_imp_eq assms(2) assms(5) assms(6) length_sts_plus 
+         plus_list_len sts_disj_test_correct sts_minus_free wf_cpg_test_disj wf_cpg_test_extrapo wf_cpg_test_len)
+  hence "wf_cpg_test sts1' c2 = (True, sts1' + sts2')"
+    by (metis all_free_plus assms(1) assms(3) assms(5) wf_cpg_test_len)
+  with assms(1)
+  show ?thesis by simp
+qed
+
+lemma c2t_seq:
+  assumes "c2t env c1 = t1"
+  and "c2t env c2 = t2"
+  shows "c2t env (CSeq c1 c2) = (t1; t2)"
+  using assms by simp
+
+lemma c2t_local:
+  assumes "\<And>x. (c2t (x#xs) cpg = body x)"
+  shows "c2t xs (CLocal cpg) = (TL x. body x)"
+  using assms
+  by simp
+
+lemma wf_cpg_test_local:
+  assumes "wf_cpg_test (Free#sts) cpg = (b, s'#sts')"
+  shows "wf_cpg_test sts (CLocal cpg) = (b, sts')"
+  by (simp add:assms)
+
+lemma wf_c2t_combined:
+  assumes "wf_cpg_test sts cpg = (True, sts)"
+  and "c2t env cpg = tpg"
+  and  "list_all (op = Free) sts"
+  and "length env = length sts"
+  shows "\<forall> i. \<exists> j s.  ((i:[tpg]:j) s)"
+proof
+  fix i
+  from wf_cpg_test_correct[OF assms(1), rule_format, of i]
+  obtain j where "c2p (sts - sts) i cpg j" by metis
+  from this[unfolded c2p_def]
+  obtain f where h: "\<forall>x. length x = length (sts - sts) \<and>
+          (\<forall>k<length (sts - sts). (sts - sts) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow>
+          Ex (i :[ c2t x cpg ]: j)" by metis
+  have "\<exists> s. (i :[ c2t env cpg ]: j) s"
+  proof(rule h[rule_format], rule conjI)
+    show "length env = length (sts - sts)"
+    by (smt assms(4) minus_list_len)
+  next
+    show "\<forall>k<length (sts - sts). (sts - sts) ! k = Bound \<longrightarrow> env ! k = f i k"
+      by (metis assms(3) minus_status.simps(1) nth_sts_minus status.distinct(1) sts_minus_free)
+  qed
+  show "\<exists> j s.  ((i:[tpg]:j) s)"
+    by (metis `\<exists>s. (i :[ c2t env cpg ]: j) s` assms(2))
+qed
+
+subsection {* The Checker *}
+
+ML {*
+  print_depth 200
+*}
+
+subsubsection {* Auxilary functions *}
+
+ML {*
+local
+  fun clear_binds ctxt = (ctxt |> Variable.binds_of |> Vartab.keys |> map (fn xi => (xi, NONE))
+                               |> fold Variable.bind_term) ctxt 
+  fun get_binds ctxt = ctxt |> Variable.binds_of |> Vartab.dest |> map (fn (xi, (_, tm)) => (xi, SOME tm))
+  fun set_binds blist ctxt = (fold Variable.bind_term blist) (clear_binds ctxt)
+in
+  fun blocalM f =      liftM (m2M (fn ctxt => returnM (get_binds ctxt)))
+                :|-- (fn binds => 
+                           f
+                      :|-- (fn result =>
+                               liftM (m2M (fn ctxt' => s2M (set_binds binds ctxt') |-- returnM result
+                                     )))
+                     )
+end
+
+  fun condM bf scan = (fn v => m0M (fn st => if (bf (v, st)) then scan v else returnM v))
+
+  local 
+    val counter = Unsynchronized.ref 0
+  in 
+    fun init_counter n = (counter := n)
+    fun counter_test x = 
+        if !counter <= 1 then true
+        else (counter := !counter - 1; false)
+  end
+
+  (* break point monad *)
+  fun bpM v' = (fn v => m0M (fn st => raiseM (v', (v, st))))
+
+  fun the_theory () = ML_Context.the_local_context () |> Proof_Context.theory_of 
+  fun the_context () = ML_Context.the_local_context ()
+
+  (* Calculating the numberal of integer [i] *)
+  fun nat_of i = if i = 0 then @{term "0::nat"} else
+                   (Const ("Num.numeral_class.numeral", @{typ "num \<Rightarrow> nat"}) $ 
+                     (Numeral.mk_cnumeral i |> term_of))
+
+  fun vfixM nm typ = (m2M' (fn ctxt => let
+         val ([x], ctxt') = Variable.variant_fixes [nm] ctxt
+         val tm_x = Free (x, typ)
+   in s2M ctxt' |-- returnM tm_x end))
+  fun fixM nm typ = (m2M' (fn ctxt => let
+         val ([x], ctxt') = Variable.add_fixes [nm] ctxt
+         val tm_x = Free (x, typ)
+   in s2M ctxt' |-- returnM tm_x end))
+  local
+    fun mk_listM l = 
+     case l of 
+       [] => @{fterm "[]"}
+     | (tm::tms) => localM (@{match "?x"} tm
+                            |-- (mk_listM tms)
+                           :|-- @{match "?xs"}
+                            |-- @{fterm "?x#?xs"})
+  in
+    fun mk_list_term ctxt l = [((), ctxt)] |> mk_listM l |> normVal |> fst
+  end
+  fun term_name (Const (x, _)) = Long_Name.base_name x
+    | term_name (Free (x, _)) = x
+    | term_name (Var ((x, _), _)) = x
+    | term_name _ = Name.uu;
+
+  val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
+
+   fun simpl_conv ss thl ctm =
+            rew_conv (ss addsimps thl) ctm RS meta_eq_to_obj_eq;
+
+  fun find_thms ctxt pats = 
+       Find_Theorems.find_theorems ctxt NONE NONE true
+               (map (fn pat =>(true, Find_Theorems.Pattern 
+                       (Proof_Context.read_term_pattern ctxt pat))) pats) |> snd |> map snd
+
+
+  fun local_on arg rhs = [((), @{context})] |>
+                         @{match "?body"} (Term.lambda arg rhs) |--
+                         @{fterm "TL x. ?body x"} |> normVal |> fst
+  fun find_idx vars l = (nat_of (find_index (equal l) vars))
+
+ local
+    fun mk_pair_term (i, j) = [((), @{context})] |> 
+            @{match "?i"} (nat_of i) 
+        |-- @{match "?j"} (nat_of j) 
+        |-- @{fterm "(?i, ?j)"} |> normVal |> fst 
+ in
+    fun mk_npair_list_term ctxt pair_list = 
+          if pair_list = [] then @{term "[]::(nat \<times> nat) list"}
+          else pair_list |> map mk_pair_term |> mk_list_term ctxt
+ end
+
+  fun list_of_array ary = let 
+     val len = Array.length ary
+     val idx = upto (0, len - 1)
+  in map (fn i => Array.sub (ary, i)) idx  end
+
+local
+    fun mk_env_term ctxt lst = 
+      if lst = [] then @{term "[]::tstate list"} else (mk_list_term ctxt lst)
+    fun mk_pair_term ctxt (i, j) = [((), ctxt)] |> 
+            @{match "?i"} (mk_env_term ctxt i)
+        |-- @{match "?j"} (nat_of j) 
+        |-- @{fterm "(?i, ?j)"} |> normVal |> fst 
+in
+    fun mk_tpair_list_term ctxt pair_list = 
+       if pair_list = [] then @{term "[] :: (tstate list \<times> nat) list"}
+       else pair_list |> map (mk_pair_term ctxt) |> mk_list_term ctxt
+end
+
+*}
+
+subsubsection {* The reifier *} 
+
+ML {*
+  fun locM (c2t_thm, test_thm) = (m1M' (fn env => 
+  let
+    val Free (x, _) = hd env 
+    val c2t_thm = Drule.generalize ([], [x]) c2t_thm
+    val c2t_thm = @{thm c2t_local} OF [c2t_thm]
+    val test_thm = @{thm wf_cpg_test_local} OF [test_thm]
+  in
+    s1M (tl env) |-- returnM (c2t_thm, test_thm)
+  end))
+
+  fun reify_local reify t = 
+      (      @{match "TL x . ?body (x::tstate)"} t 
+         |-- vfixM "x" @{typ "tstate"}
+        :|-- @{match "?x"}
+        :|-- (fn tmx => m1M' (fn env => s1M (tmx::env)))
+         |-- @{fterm "?body ?x"}
+        :|-- reify 
+        :|-- locM 
+        (* :|-- condM counter_test (bpM ("local", t))  *)
+      )
+ 
+  fun labelM exp = m0M' (fn (env, ctxt) => let
+  (* The following three lines are used for debugging purpose
+       (* (* The following two lines are used to set breakpoint counter
+                 and invoke the reifyer in debug mode *)
+         val _ = init_counter 3
+         val t = reify tpg_def_rhs [(rev tpg_def_largs_sufx, ctxt_tpg_def)] |> normExcp 
+       *)
+       (* The following line is used to extract break point information and 
+          establish the environment to execute body statements *)
+       val ((brc, exp), (_, (env, ctxt)::_)) = t 
+  *)
+  val c2t_thm = [((), ctxt)] |>
+           @{match "?cpg"} exp
+        |-- @{match "?env"} (env |> mk_list_term ctxt)
+        |-- @{fterm "c2t ?env ?cpg"} |> normVal |> fst |> cterm_of (Proof_Context.theory_of ctxt) 
+                     |> simpl_conv (simpset_of ctxt) []
+  val test_thm = [((), ctxt)] |>
+           @{match "?cpg"} exp
+        |-- @{match "?sts"} (env |> map (fn _ => @{term "Free"}) |> mk_list_term ctxt)
+        |-- @{fterm "wf_cpg_test ?sts ?cpg"} |> normVal |> fst |> cterm_of (Proof_Context.theory_of ctxt) 
+                     |> simpl_conv (simpset_of ctxt) []
+   in returnM (c2t_thm, test_thm) end)
+
+   fun reify_label t = 
+             @{match "TLabel ?L"} t 
+         |-- @{fterm "?L"} 
+        :|-- (fn l => m1M' (fn st => returnM (find_idx st l))) 
+        :|-- @{match ?L1} 
+         |-- @{fterm "CLabel ?L1"}
+        (* :|-- condM counter_test (bpM ("label", t)) *)
+        :|-- labelM
+
+  fun seqM ((c2t_thm1, test_thm1), (c2t_thm2, test_thm2)) =
+  m0M' (fn (env, ctxt) =>
+  let
+     val simp_trans = (simpset_of ctxt) delsimps @{thms wf_cpg_test.simps c2t.simps} |> full_simplify
+     val ct2_thm = (@{thm c2t_seq} OF [c2t_thm1, c2t_thm2]) |> simp_trans
+     val test_thm =  (@{thm wf_cpg_test_seq} OF [test_thm1, test_thm2]) |> simp_trans
+  in returnM (ct2_thm, test_thm) end)
+
+   fun reify_seq reify t = 
+             @{match "?c1; ?c2"} t 
+         |-- ((@{fterm "?c1"} :|-- reify) -- 
+              (@{fterm "?c2"} :|-- reify))
+        (* :|-- condM counter_test (bpM ("seq", t))  *)
+        :|-- seqM
+
+  fun reify_instr t = 
+             @{match "\<guillemotright> ((?A0, ?L0), (?A1, ?L1))"} t 
+         |-- @{fterm "?L0"} 
+        :|-- (fn l => m1M' (fn st => returnM (find_idx st l))) 
+        :|-- @{match ?L0'} 
+         |-- @{fterm "?L1"} 
+        :|-- (fn l => m1M' (fn st => returnM (find_idx st l))) 
+        :|-- @{match ?L1'} 
+         |-- @{fterm "CInstr ((?A0, ?L0'), (?A1, St ?L1'))"}
+        :|-- labelM
+        (* :|-- condM counter_test (bpM ("instr", t)) *)
+
+  fun reify_var var = 
+    (* condM counter_test (bpM ("var", var)) () |--  *)
+  (m0M' (fn (env, ctxt) => let
+  (* The following three lines are used for debugging purpose
+       (* (* The following two lines are used to set breakpoint counter
+                 and invoke the reifyer in debug mode *)
+         val _ = init_counter 3
+         val t = reify tpg_def_rhs [(rev tpg_def_largs_sufx, ctxt_tpg_def)] |> normExcp 
+       *)
+       (* The following line is used to extract break point information and 
+          establish the environment to execute body statements *)
+       val ((brc, var), (_, (env, ctxt)::_)) = t 
+  *)
+  val (var_hd, var_args) = Term.strip_comb var
+  val (var_args_prefx, var_args_sufx) = 
+            take_suffix (fn tm => type_of tm = @{typ "tstate"}) var_args
+  val var_skel_hd_typ = var_args_prefx |> map type_of |> (fn typs => typs ---> @{typ "cpg"})
+  (* We discriminate two cases, one for tpg constants; the other for argument variable *)
+  val  ([var_skel_hd_name], ctxt1) = 
+      case var_hd of
+        (Const (nm, _)) => ([((nm |> Long_Name.base_name)^"_skel")], ctxt)
+      | _ =>  Variable.variant_fixes [(term_name var_hd^"_skel_")] ctxt
+  (* If [var_hd] is a constant, a corresponding skeleton constant is assumed to exist alrady *)
+  val var_skel_hd = if (Term.is_Const var_hd) then  Syntax.read_term ctxt1 var_skel_hd_name
+                    else Free (var_skel_hd_name, var_skel_hd_typ)
+  (* [skel_tm] is the skeleton object the properties of which will either be assumed (in case of 
+     argument variable), or proved (in case of global constants ) *)
+  val skel_tm = Term.list_comb (var_skel_hd, var_args_prefx) 
+  (* Start to prove or assume [c2t] property (named [c2t_thm]) of the skeleton object, 
+     since the [c2t] property needs to be universally qantified, we 
+     need to invent quantifier names: *)
+  val (var_skel_args_sufx_names, ctxt2) = 
+              Variable.variant_fixes (var_args_sufx |> map term_name) ctxt1
+  val var_skel_args_sufx = var_skel_args_sufx_names |> map (fn nm => Free (nm, @{typ "tstate"}))
+  val c2t_rhs = Term.list_comb (var_hd, var_args_prefx@var_skel_args_sufx)
+  val c2t_env = mk_list_term ctxt2 (var_skel_args_sufx |> rev) 
+  val eqn = [((), ctxt2)] |>
+           @{match ?env} c2t_env
+       |-- @{match ?skel_tm} skel_tm
+       |-- @{match ?c2t_rhs} c2t_rhs
+       |-- @{fterm "Trueprop (c2t ?env ?skel_tm = ?c2t_rhs)"} |> normVal |> fst 
+  fun all_on ctxt arg body = Const ("all", dummyT) $ (Term.lambda arg body) |> 
+            Syntax.check_term ctxt
+  val c2t_eqn = fold (all_on ctxt2) (rev var_skel_args_sufx) eqn |> cterm_of (Proof_Context.theory_of ctxt2)
+  val ([c2t_thm], ctxt3) = 
+       if (Term.is_Const var_hd) then 
+          (* if [var_hd] is an constant, try to prove [c2t_eqn] by searching 
+             into the facts database *)
+          let
+               val pat_skel_args = fold (curry (op ^)) (map (K  " _ ")  var_args_prefx) ""
+               val pat_skel_str = "( "^ var_skel_hd_name ^ pat_skel_args ^" )"
+               val test_pat = ("wf_cpg_test _ "^ pat_skel_str ^" = (True, _)")
+               val c2t_pat = ("c2t _ "^ pat_skel_str ^" = _")
+               val (wf_test_thms, c2t_thms) = ([test_pat], [c2t_pat]) |> pairself (find_thms ctxt2)
+          in
+             ([([((0, @{thm "refl"}), ctxt2)] |>
+                  goalM (c2t_eqn |> term_of)
+               |-- tacM (fn ctxt => (Simplifier.simp_tac ((simpset_of ctxt) addsimps c2t_thms) 1))
+               >> Goal.conclude |> normVal |> fst |> Raw_Simplifier.norm_hhf)], ctxt2)
+          end
+       else (* Otherwise, make [c2t_eqn] an assumption *) 
+          Assumption.add_assumes [c2t_eqn] ctxt2
+  (* Start to prove or assume [wf_cpg_test] property (named [wf_test_thm]) of the skeleton object. *)
+  val sts = map (fn tm => @{term "Free"}) var_args_sufx |> mk_list_term ctxt3 
+  val wf_test_eqn = [((), ctxt3)] |>
+           @{match ?cpg} skel_tm
+       |-- @{match ?sts} sts
+       |-- @{fterm "Trueprop (wf_cpg_test ?sts ?cpg = (True, ?sts))"} |> normVal |> fst 
+              |> cterm_of (Proof_Context.theory_of ctxt3)
+  val ([wf_test_thm], ctxt4) =
+       if (Term.is_Const var_hd) then 
+          let
+               val pat_skel_args = fold (curry (op ^)) (map (K  " _ ")  var_args_prefx) ""
+               val pat_skel_str = "( "^ var_skel_hd_name ^ pat_skel_args ^ " )"
+               val test_pat = ("wf_cpg_test _ "^ pat_skel_str ^" = (True, _)")
+               val c2t_pat = ("c2t _ "^ pat_skel_str ^" = _")
+               val wf_test_thms = [test_pat] |> (find_thms ctxt2)
+          in
+             ([([((0, @{thm "refl"}), ctxt2)] |>
+                  goalM (wf_test_eqn |> term_of)
+               |-- tacM (fn ctxt => (Simplifier.simp_tac ((simpset_of ctxt) addsimps wf_test_thms) 1))
+               >> Goal.conclude |> normVal |> fst |> Raw_Simplifier.norm_hhf)], ctxt3)
+          end
+       else Assumption.add_assumes [wf_test_eqn] ctxt3
+  (* Start the derivation of the length theorem *)
+  val length_env = mk_list_term ctxt4 (var_args_sufx  |> rev)
+  val length_thm = [((0, @{thm "init"}), ctxt4)] |>
+          @{match "(?env)"} length_env
+       |-- @{match "(?sts)"} sts
+       |-- @{fterm "Trueprop (length (?env::tstate list) = length (?sts::status list))"}
+      :|-- goalM
+       |-- tacM (fn ctxt => (Simplifier.simp_tac (simpset_of ctxt) 1))
+            >> Goal.conclude |> normVal |> fst 
+  (* Start compute two adjust operations, namely [sps] and [lfs] *)
+  val locs = var_args_sufx |> map (fn arg => find_index (equal arg) env) |> rev
+  val swaps = swaps_of locs
+  val sps = swaps |> mk_npair_list_term @{context} 
+  val locs' = sexec swaps (Array.fromList locs) |> list_of_array
+  val pairs = ((~1::locs') ~~ (locs' @ [length env]))
+  fun lfs_of (t, ops) [] = ops |> rev
+    | lfs_of (t, ops) ((i, j)::pairs) = let
+          val stuf = upto (i + 1, j - 1) |> map (fn idx => nth env idx)
+      in if (stuf <> []) then lfs_of (t + length stuf + 1, (stuf, t)::ops) pairs 
+                        else lfs_of (t + length stuf + 1, ops) pairs 
+      end
+  val lfs = lfs_of (0, []) pairs |> mk_tpair_list_term @{context} 
+  (* [simp_trans] is the simplification procedure used to simply the theorem after 
+     instantiation.
+  *)
+  val simp_trans =  full_simplify ((simpset_of @{context}) addsimps @{thms adjust_sts_def
+                               adjust_env_def perm_s_def perm_b_def map_idx_len 
+                                     map_idx_def upto_map upto_empty} @ [c2t_thm])
+  (* Instantiating adjust theorems *)
+  val adjust_c2t_thm = [((), ctxt4)] |>  
+                @{match "?sps"} sps 
+            |-- @{match "?lfs"} lfs 
+            |-- thm_instM (@{thm adjust_c2t} OF [wf_test_thm, length_thm]) 
+                   |> normVal |> fst |> simp_trans
+  val adjust_test_thm = [((), ctxt4)] |>  
+                @{match "?sps"} sps 
+            |-- @{match "?lfs"} lfs 
+            |-- thm_instM (@{thm adjust_wf_cpg_test} OF [wf_test_thm]) 
+                   |> normVal |> fst |> simp_trans
+ in 
+    (* s2M ctxt4 |-- *) returnM (adjust_c2t_thm, adjust_test_thm)
+end)) 
+
+  fun reify t = 
+      localM (reify_seq reify t || 
+      reify_local reify t ||
+      reify_label t || 
+      reify_instr t ||
+      reify_var t
+     )
+*}
+
+subsubsection {* The Checker packed up as the asmb attribute *}
+
+ML {*
+ fun asmb_attrib def_thm = 
+  Context.cases (fn thy =>
+  (* val thy = @{theory} *) let 
+  fun thy_exit ctxt = 
+       Context.Theory (Local_Theory.exit_global (Local_Theory.assert_bottom true ctxt))
+  val ctxt0 = Named_Target.theory_init thy
+  val (((x, y), [tpg_def]), ctxt_tpg_def) = Variable.import true [def_thm] ctxt0
+  val (tpg_def_lhs, tpg_def_rhs) = [((), ctxt_tpg_def)] |> 
+                   @{match "Trueprop (?L = ?R)"} (prop_of tpg_def) 
+               |-- @{fterm "?L"} -- @{fterm "?R"} |> normVal |> fst
+  val (tpg_def_lhd, tpg_def_largs) = Term.strip_comb tpg_def_lhs
+  val (tpg_def_largs_prefx, tpg_def_largs_sufx) = 
+                 take_suffix (fn tm => type_of tm = @{typ "tstate"}) tpg_def_largs
+  (* Invoking the reifyer in normal mode *)
+  val ((c2t_thm_1, test_thm_1), ((_, ctxt_r)::y)) = 
+          reify tpg_def_rhs [(rev tpg_def_largs_sufx, ctxt_tpg_def)] 
+            |> normVal
+  val asmb_thm_1 = (@{thm wf_c2t_combined} OF [test_thm_1, c2t_thm_1]) |> (full_simplify (simpset_of ctxt_r))
+  val (r_cpg, r_tpg) = [((), ctxt_r)] |> 
+             @{match "Trueprop (c2t _ ?X = ?tpg)"} (c2t_thm_1 |> prop_of)
+          |-- (@{fterm "?X"} -- @{fterm "?tpg"}) |> normVal |> fst 
+  val tpg_def_params = Variable.add_fixed ctxt_tpg_def (tpg_def_lhs) [] |> map fst
+          |> sort (Variable.fixed_ord ctxt_tpg_def)
+  val r_cpg_frees = Term.add_frees r_cpg []
+  local fun condense [] = []
+          | condense xs = [hd xs]
+  in
+  val skel_def_params = 
+            tpg_def_params |> map (fn nm => condense 
+                                          (filter (fn (tnm, _) => String.isPrefix nm tnm) r_cpg_frees))
+                |> flat |> map Free
+  end      
+  val skel_def_rhs = fold Term.lambda (skel_def_params |> rev) r_cpg 
+  local
+     val Const (nm, _) = tpg_def_lhs |> Term.head_of 
+  in
+     val tpg_def_name = nm |> Long_Name.base_name
+     val skel_def_lhs = Free (tpg_def_name^"_skel", type_of skel_def_rhs)
+  end
+  val skel_def_eqn = [((), ctxt_r)] |> 
+             @{match "?lhs"} skel_def_lhs
+         |-- @{match "?rhs"} skel_def_rhs
+         |-- @{fterm "Trueprop (?lhs = ?rhs)"} |> normVal |> fst 
+  val ((skel_def_lhs, (skel_def_name, skel_def_thm)), lthy2) = 
+       Specification.definition (NONE, (Attrib.empty_binding, skel_def_eqn)) ctxt_r
+  val c2t_thm_final = [((0, @{thm refl}), lthy2)] |> 
+            @{match "?env"} (mk_list_term lthy2 (rev tpg_def_largs_sufx))
+        |-- @{match "?skel"} (Term.list_comb (skel_def_lhs, skel_def_params))
+  val c2t_thm_final = [((0, @{thm refl}), lthy2)] |> 
+            @{match "?env"} (mk_list_term lthy2 (rev tpg_def_largs_sufx))
+        |-- @{match "?skel"} (Term.list_comb (skel_def_lhs, skel_def_params))
+        |-- @{match "?tpg"} tpg_def_lhs
+        |-- @{fterm "Trueprop (c2t ?env ?skel = ?tpg)"} 
+       :|-- goalM
+        |-- tacM (fn ctxt => (Simplifier.simp_tac ((simpset_of ctxt |> Simplifier.clear_ss) 
+                            addsimps [skel_def_thm, c2t_thm_1]) 1))
+        |-- tacM (fn  ctxt => (Simplifier.simp_tac ((simpset_of ctxt |> Simplifier.clear_ss) 
+                            addsimps [def_thm]) 1))
+            >> Goal.conclude |> normVal |> fst
+  val test_thm_final = [((0, @{thm refl}), lthy2)] |> 
+            @{match "?sts"} (tpg_def_largs_sufx |> map (fn _ => @{term "Free"}) |> mk_list_term lthy2)
+        |-- @{match "?skel"} (Term.list_comb (skel_def_lhs, skel_def_params))
+        |-- @{fterm "Trueprop (wf_cpg_test ?sts ?skel = (True, ?sts))"} 
+       :|-- goalM
+        |-- tacM (fn ctxt => (Simplifier.simp_tac ((simpset_of ctxt |> Simplifier.clear_ss) 
+                            addsimps [skel_def_thm, test_thm_1]) 1))
+              >> Goal.conclude |> normVal |> fst 
+  val asmb_thm_final = [((0, @{thm refl}), lthy2)] |> 
+            @{match "?tpg"} tpg_def_lhs
+        |-- @{fterm "Trueprop (\<forall> i. \<exists> j s. (i:[?tpg]:j) s)"} 
+       :|-- goalM
+        |-- tacM (fn ctxt => (Simplifier.simp_tac ((simpset_of ctxt) 
+                            addsimps [tpg_def, asmb_thm_1]) 1))
+         >> Goal.conclude |> normVal |> fst 
+  fun generalize thm = let
+    val hyps = (#hyps (thm |> Thm.crep_thm))
+    val thm' =  if (length hyps = 0) then thm 
+                else (fold Thm.implies_intr (#hyps (thm |> Thm.crep_thm) |> rev |> tl |> rev) thm)
+  in
+      thm' |> Thm.forall_intr_frees 
+  end
+  val lthy3 = 
+         Local_Theory.note ((Binding.name ("c2t_" ^ tpg_def_name ^ "_skel"), []), 
+                      [c2t_thm_final |> generalize]) lthy2 |> snd
+  val lthy4 = 
+         Local_Theory.note ((Binding.name ("wf_" ^ tpg_def_name ^ "_skel"), []), 
+                      [test_thm_final |> generalize]) lthy3 |> snd
+  val lthy5 = 
+         Local_Theory.note ((Binding.name ("asmb_" ^ tpg_def_name), []), 
+                      [asmb_thm_final |> Drule.export_without_context]) lthy4 |> snd
+in 
+  thy_exit lthy5
+end) (fn ctxt => Context.Proof ctxt)
+*}
+
+setup {*
+  Attrib.setup @{binding asmb} (Scan.succeed (Thm.declaration_attribute asmb_attrib)) "asmb attribute"
+*}
+
+
+section {* Basic macros for TM *}
+
+definition [asmb]: "write_zero = (TL exit. \<guillemotright>((W0, exit), (W0, exit)); TLabel exit)"
+
+definition [asmb]: "write_one = (TL exit. \<guillemotright>((W1, exit), (W1, exit)); TLabel exit)"
+
+definition [asmb]: "move_left = (TL exit . \<guillemotright>((L, exit), (L, exit)); TLabel exit)"
+
+definition [asmb]: "move_right = (TL exit . \<guillemotright>((R, exit), (R, exit)); TLabel exit)"
+
+definition [asmb]: "if_one e = (TL exit . \<guillemotright>((W0, exit), (W1, e)); TLabel exit)"
+
+definition [asmb]: "if_zero e = (TL exit . \<guillemotright>((W0, e), (W1, exit)); TLabel exit)"
+
+definition [asmb]: "jmp e = \<guillemotright>((W0, e), (W1, e))"
+
+definition [asmb]: 
+          "right_until_zero = 
+                 (TL start exit. 
+                  TLabel start;
+                     if_zero exit;
+                     move_right;
+                     jmp start;
+                  TLabel exit
+                 )"
+
+definition [asmb]: 
+       "left_until_zero = 
+                 (TL start exit. 
+                  TLabel start;
+                    if_zero exit;
+                    move_left;
+                    jmp start;
+                  TLabel exit
+                 )"
+
+definition [asmb]: 
+       "right_until_one = 
+                 (TL start exit. 
+                  TLabel start;
+                     if_one exit;
+                     move_right;
+                     jmp start;
+                  TLabel exit
+                 )"
+
+definition [asmb]: 
+          "left_until_one = 
+                 (TL start exit. 
+                  TLabel start;
+                    if_one exit;
+                    move_left;
+                    jmp start;
+                  TLabel exit
+                 )"
+
+definition [asmb]: 
+    "left_until_double_zero = 
+            (TL start exit.
+              TLabel start;
+              if_zero exit;
+              left_until_zero;
+              move_left;
+              if_one start;
+              TLabel exit)"
+
+definition [asmb]: 
+        "shift_right =
+            (TL start exit.
+              TLabel start;
+                 if_zero exit;
+                 write_zero;
+                 move_right;
+                 right_until_zero;
+                 write_one;
+                 move_right;
+                 jmp start;
+              TLabel exit
+            )"
+
+definition [asmb]: 
+        "clear_until_zero = 
+             (TL start exit.
+              TLabel start;
+                 if_zero exit;
+                 write_zero;
+                 move_right;
+                 jmp start;
+              TLabel exit)"
+
+definition [asmb]: 
+      "shift_left = 
+            (TL start exit.
+              TLabel start;
+                 if_zero exit;
+                 move_left;
+                 write_one;
+                 right_until_zero;
+                 move_left;
+                 write_zero;
+                 move_right;
+                 move_right;
+                 jmp start;
+              TLabel exit)
+           "
+
+definition [asmb]: 
+       "bone c1 c2 = (TL exit l_one.
+                                if_one l_one;
+                                  (c1;
+                                   jmp exit);
+                                TLabel l_one;
+                                      c2;
+                                TLabel exit
+                              )"
+
+definition [asmb]: 
+             "cfill_until_one = (TL start exit.
+                                TLabel start;
+                                  if_one exit;
+                                  write_one;
+                                  move_left;
+                                  jmp start;
+                                TLabel exit
+                               )"
+
+definition [asmb]:
+          "cmove = (TL start exit.
+                       TLabel start;
+                         left_until_zero;
+                         left_until_one;
+                         move_left;
+                         if_zero exit;
+                         move_right;
+                         write_zero;
+                         right_until_one;
+                         right_until_zero;
+                         write_one;
+                         jmp start;
+                     TLabel exit
+                    )"
+
+definition [asmb]: 
+           "cinit = (right_until_zero; move_right; write_one)"
+
+definition [asmb]:
+           "copy = (cinit; cmove; move_right; move_right; right_until_one; 
+               move_left; move_left; cfill_until_one)"
+
+definition  
+         "bzero c1 c2 = (TL exit l_zero.
+                                if_zero l_zero;
+                                  (c1;
+                                   jmp exit);
+                                TLabel l_zero;
+                                      c2;
+                                TLabel exit
+                              )"
+
+definition  "if_reps_nz e = (move_right;
+                              bzero (move_left; jmp e) (move_left)
+                           )"
+
+declare if_reps_nz_def[unfolded bzero_def, asmb]
+
+definition "if_reps_z e = (move_right;
+                              bone (move_left; jmp e) (move_left)
+                             )"
+
+declare if_reps_z_def [unfolded bone_def, asmb]
+
+definition 
+           "skip_or_set = bone (write_one; move_right; move_right)
+                               (right_until_zero; move_right)"
+
+declare skip_or_set_def[unfolded bone_def, asmb]
+
+definition "tpg_fold tpgs = foldr TSeq (butlast tpgs) (last tpgs)"
+
+definition "cpg_fold cpgs = foldr CSeq (butlast cpgs) (last cpgs)"
+
+definition "skip_or_sets n = tpg_fold (replicate n skip_or_set)"
+
+definition "skip_or_sets_skel n = cpg_fold (replicate n skip_or_set_skel)"
+
+lemma c2t_skip_or_sets_skel: 
+    "c2t [] (skip_or_sets_skel (Suc n)) = skip_or_sets (Suc n)"
+proof(induct n)
+  case (Suc k)
+  thus ?case 
+    apply (unfold skip_or_sets_skel_def cpg_fold_def skip_or_sets_def tpg_fold_def)
+    my_block
+      fix x k
+      have "(last (replicate (Suc k) x)) = x"
+        by (metis Suc_neq_Zero last_replicate)
+    my_block_end
+    apply (unfold this)
+    my_block
+      fix x k
+      have "(butlast (replicate (Suc k) x)) = replicate k x"
+        by (metis butlast_snoc replicate_Suc replicate_append_same)
+    my_block_end
+    apply (unfold this)
+    my_block
+      fix x k f y
+      have "foldr f (replicate (Suc k) x) y =  f x (foldr f (replicate k x) y)"
+        by simp
+    my_block_end
+    apply (unfold this)
+    by (simp add:c2t_skip_or_set_skel)
+next
+  case 0
+  show ?case
+   by (simp add:skip_or_sets_skel_def cpg_fold_def skip_or_sets_def tpg_fold_def
+             c2t_skip_or_set_skel)
+qed
+
+lemma wf_skip_or_sets_skel: 
+    "wf_cpg_test [] (skip_or_sets_skel (Suc n)) = (True, [])"
+proof(induct n)
+  case (Suc k)
+  thus ?case
+   apply (unfold skip_or_sets_skel_def cpg_fold_def)
+    my_block
+      fix x k
+      have "(last (replicate (Suc k) x)) = x"
+        by (metis Suc_neq_Zero last_replicate)
+    my_block_end
+    apply (unfold this)
+    my_block
+      fix x k
+      have "(butlast (replicate (Suc k) x)) = replicate k x"
+        by (metis butlast_snoc replicate_Suc replicate_append_same)
+    my_block_end
+    apply (unfold this)
+    my_block
+      fix x k f y
+      have "foldr f (replicate (Suc k) x) y =  f x (foldr f (replicate k x) y)"
+        by simp
+    my_block_end
+    apply (unfold this)
+    by (simp add:wf_skip_or_set_skel)
+next
+  case 0
+  thus ?case
+    apply (unfold skip_or_sets_skel_def cpg_fold_def)
+    by (simp add:wf_skip_or_set_skel)
+qed
+
+lemma asmb_skip_or_sets: 
+   "\<forall>i. \<exists>j s. (i :[ skip_or_sets (Suc n) ]: j) s"
+  by (rule wf_c2t_combined[OF wf_skip_or_sets_skel c2t_skip_or_sets_skel], auto)
+
+definition [asmb]: "locate n = (skip_or_sets (Suc n);
+                        move_left;
+                        move_left;
+                        left_until_zero;
+                        move_right
+                       )"
+
+definition [asmb]: "Inc a = locate a; 
+                    right_until_zero; 
+                    move_right;
+                    shift_right;
+                    move_left;
+                    left_until_double_zero;
+                    write_one;
+                    left_until_double_zero;
+                    move_right;
+                    move_right
+                    "
+
+definition [asmb]: "Dec a e  = (TL continue. 
+                          (locate a; 
+                           if_reps_nz continue;
+                           left_until_double_zero;
+                           move_right;
+                           move_right;
+                           jmp e);
+                          (TLabel continue;
+                           right_until_zero; 
+                           move_left;
+                           write_zero;
+                           move_right;
+                           move_right;
+                           shift_left;
+                           move_left;
+                           move_left;
+                           move_left;
+                           left_until_double_zero;
+                           move_right;
+                           move_right))"
+
+end
\ No newline at end of file