Theory ComposableTMs

(* Title: thys/ComposableTMs.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
   Modifications: Sebastiaan Joosten
 
   Modifications and comments by Franz Regensburger (FABR) 02/2022

   * added function mk_composable0 that generates composable TMs from non-composable TMs
     such that the overall behaviour of the TM is preserved.

     This is important for the proof of the existence of uncomputable functions
     respectively undecidable sets and relations.
 *)

theory ComposableTMs
  imports Turing
begin

section ‹Making Turing Machines composable›

(* Well-formedness of Turing machine programs
 *
 * For certain inputs programs tm with ¬(composable_tm tm) may reach
 * the final state with a standard tape!
 *
 * These machines are no junk. They are simply not composable via |+|
 *)

abbreviation "is_even n ≡ (n::nat) mod 2 = 0"
abbreviation "is_odd n ≡ (n::nat) mod 2 ≠ 0"

fun 
  composable_tm :: "tprog ⇒ bool"
  where
    "composable_tm (p, off) = (length p ≥ 2 ∧ is_even (length p) ∧ 
                    (∀(a, s) ∈ set p. s ≤ length p div 2 + off ∧ s ≥ off))"

abbreviation
  "composable_tm0 p ≡ composable_tm (p, 0)"

lemma step_in_range: 
  assumes h1: "¬ is_final (step0 c A)"
    and h2: "composable_tm (A, 0)"
  shows "fst (step0 c A) ≤ length A div 2"
  using h1 h2
  apply(cases c;cases "fst c";cases "hd (snd (snd c))")
  by(auto simp add: Let_def case_prod_beta')

lemma steps_in_range: 
  assumes h1: "¬ is_final (steps0 (1, tap) A stp)"
    and h2: "composable_tm (A, 0)"
  shows "fst (steps0 (1, tap) A stp) ≤ length A div 2"
  using h1
proof(induct stp)
  case 0
  then show "fst (steps0 (1, tap) A 0) ≤ length A div 2" using h2
    by (auto)
next
  case (Suc stp)
  have ih: "¬ is_final (steps0 (1, tap) A stp) ⟹ fst (steps0 (1, tap) A stp) ≤ length A div 2" by fact
  have h: "¬ is_final (steps0 (1, tap) A (Suc stp))" by fact
  from ih h h2 show "fst (steps0 (1, tap) A (Suc stp)) ≤ length A div 2"
    by (metis step_in_range step_red)
qed

(* ------------------------------------------------------------------------ *)
(* New by FABR                                                              *)
(* ------------------------------------------------------------------------ *)

subsection ‹Definitin of function fix\_jumps and mk\_composable0›

fun fix_jumps  :: "nat ⇒ tprog0 ⇒ tprog0" where
  "fix_jumps smax [] = []" |
  "fix_jumps smax (ins#inss) = (if (snd ins) ≤ smax
                                then ins # fix_jumps smax inss
                                else ((fst ins),0)#fix_jumps smax inss)"

fun mk_composable0 :: "tprog0 ⇒ tprog0" where
  "mk_composable0 []   = [(Nop,0),(Nop,0)]" |
  "mk_composable0 [i1] = fix_jumps 1 [i1,(Nop,0)]" |
  "mk_composable0 (i1#i2#ins) = (let l = 2 + length ins
                        in if is_even l
                           then fix_jumps (l div 2)       (i1#i2#ins)
                           else fix_jumps ((l div 2) + 1) ((i1#i2#ins)@[(Nop,0)]))"


subsection ‹Properties of function fix\_jumps›

lemma fix_jumps_len: "length (fix_jumps smax insl) = length insl"
  by (induct insl) auto

lemma fix_jumps_le_smax: "∀x ∈ set (fix_jumps smax tm). (snd x) ≤ smax"
proof (rule filter_id_conv[THEN iffD1])
  show "filter (λx. snd x ≤ smax) (fix_jumps smax tm) = fix_jumps smax tm"
    by (induct tm)(auto)
qed

lemma fix_jumps_nth_no_fix:
  assumes "n < length tm" and "tm!n = ins" and "(snd ins) ≤ smax"
  shows "(fix_jumps smax tm)!n = ins"
proof -
  have "n < length tm ∧ tm!n = ins ∧ (snd ins) ≤ smax ⟶ (fix_jumps smax tm)!n = ins"
  proof (induct tm arbitrary: n ins)
    case Nil
    then show ?case by auto
  next
    fix a tm n ins
    assume IV: "⋀n' ins'. n' < length tm ∧ tm ! n' = ins' ∧ snd ins' ≤ smax ⟶ fix_jumps smax tm ! n' = ins'"
    show "n < length (a # tm) ∧ (a # tm) ! n = ins ∧ snd ins ≤ smax ⟶ fix_jumps smax (a # tm) ! n = ins"
    proof (cases n)
      case 0
      then show ?thesis by auto
    next
      fix nat
      assume "n = Suc nat"
      show "n < length (a # tm) ∧ (a # tm) ! n = ins ∧ snd ins ≤ smax ⟶ fix_jumps smax (a # tm) ! n = ins"
      proof
        assume A: "n < length (a # tm) ∧ (a # tm) ! n = ins ∧ snd ins ≤ smax"
        show "fix_jumps smax (a # tm) ! n = ins"
        proof (cases "(snd a) ≤ smax")
          case True
          then have "fix_jumps smax (a # tm) ! (Suc nat) =  (a # (fix_jumps smax tm)) ! Suc nat" by auto
          also have "... = (fix_jumps smax tm) !nat" by auto
          finally have "fix_jumps smax (a # tm) ! Suc nat = (fix_jumps smax tm) !nat" by auto
          also with ‹n = Suc nat› A and IV have "... = ins" by auto
          finally have "fix_jumps smax (a # tm) ! Suc nat = ins" by auto
          with ‹n = Suc nat› show "fix_jumps smax (a # tm) ! n = ins" by auto
        next
          case False
          then have "fix_jumps smax (a # tm) ! (Suc nat) =  (((fst a),0) # (fix_jumps smax tm)) ! Suc nat" by auto
          also have "... = (fix_jumps smax tm) !nat" by auto
          finally have "fix_jumps smax (a # tm) ! Suc nat = (fix_jumps smax tm) !nat" by auto
          also with ‹n = Suc nat› A and IV have "... = ins" by auto
          finally have "fix_jumps smax (a # tm) ! Suc nat = ins" by auto
          with ‹n = Suc nat› show "fix_jumps smax (a # tm) ! n = ins" by auto
        qed
      qed
    qed
  qed
  with assms show ?thesis by auto
qed

lemma fix_jumps_nth_fix:
  assumes "n < length tm" and "tm!n = ins" and "¬(snd ins) ≤ smax"
  shows "(fix_jumps smax tm)!n = ((fst ins),0)"
proof -
  have "n < length tm ∧ tm!n = ins ∧ ¬(snd ins) ≤ smax ⟶ (fix_jumps smax tm)!n = ((fst ins),0)"
  proof (induct tm arbitrary: n ins)
    case Nil
    then show ?case by auto
  next
    fix a tm n ins
    assume IV: "⋀n' ins'. n' < length tm ∧ tm ! n' = ins' ∧ ¬(snd ins') ≤ smax ⟶ fix_jumps smax tm ! n' = (fst ins', 0)"
    show "n < length (a # tm) ∧ (a # tm) ! n = ins ∧ ¬ snd ins ≤ smax ⟶ fix_jumps smax (a # tm) ! n = (fst ins, 0)"
    proof (cases n)
      case 0
      then show ?thesis by auto
    next
      fix nat
      assume "n = Suc nat"
      show "n < length (a # tm) ∧ (a # tm) ! n = ins ∧ ¬ snd ins ≤ smax ⟶ fix_jumps smax (a # tm) ! n = (fst ins, 0)"
      proof
        assume A: "n < length (a # tm) ∧ (a # tm) ! n = ins ∧ ¬ snd ins ≤ smax"
        show "fix_jumps smax (a # tm) ! n = (fst ins, 0)"
        proof (cases "(snd a) ≤ smax")
          case True
          then have "fix_jumps smax (a # tm) ! (Suc nat) =  (a # (fix_jumps smax tm)) ! Suc nat" by auto
          also have "... = (fix_jumps smax tm) !nat" by auto
          finally have "fix_jumps smax (a # tm) ! Suc nat = (fix_jumps smax tm) !nat" by auto
          also with ‹n = Suc nat› A and IV have "... = (fst ins, 0)" by auto
          finally have "fix_jumps smax (a # tm) ! Suc nat = (fst ins, 0)" by auto
          with ‹n = Suc nat› show "fix_jumps smax (a # tm) ! n = (fst ins, 0)" by auto
        next
          case False
          then have "fix_jumps smax (a # tm) ! (Suc nat) =  (((fst a),0) # (fix_jumps smax tm)) ! Suc nat" by auto
          also have "... = (fix_jumps smax tm) !nat" by auto
          finally have "fix_jumps smax (a # tm) ! Suc nat = (fix_jumps smax tm) !nat" by auto
          also with ‹n = Suc nat› A and IV have "... = (fst ins, 0)" by auto
          finally have "fix_jumps smax (a # tm) ! Suc nat = (fst ins, 0)" by auto
          with ‹n = Suc nat› show "fix_jumps smax (a # tm) ! n = (fst ins, 0)" by auto
        qed
      qed
    qed
  qed
  with assms show ?thesis by auto
qed

subsection ‹Functions fix\_jumps and mk\_composable0 generate composable Turing Machines.›

lemma composable_tm0_fix_jumps_pre:
  assumes "length tm ≥ 2" and "is_even (length tm)"
  shows "length (fix_jumps (length tm div 2) tm) ≥ 2 ∧
          is_even (length (fix_jumps (length tm div 2) tm)) ∧ 
          (∀x ∈ set (fix_jumps (length tm div 2) tm).
             (snd x) ≤ length (fix_jumps (length tm div 2) tm) div 2 + 0 ∧ (snd x) ≥ 0)"
proof
  show "2 ≤ length (fix_jumps (length tm div 2) tm)"
    using assms by (auto simp add: fix_jumps_len)
next
  show "is_even (length (fix_jumps (length tm div 2) tm)) ∧
        (∀x∈set (fix_jumps (length tm div 2) tm). snd x ≤ length (fix_jumps (length tm div 2) tm) div 2 + 0 ∧ 0 ≤ snd x)"
  proof
    show "is_even (length (fix_jumps (length tm div 2) tm))"
      using assms by (auto simp add: fix_jumps_len)
  next
    show "∀x∈set (fix_jumps (length tm div 2) tm). snd x ≤ length (fix_jumps (length tm div 2) tm) div 2 + 0 ∧ 0 ≤ snd x"
      by (auto simp add: fix_jumps_le_smax fix_jumps_len)
  qed
qed

lemma composable_tm0_fix_jumps:
  assumes "length tm ≥ 2" and "is_even (length tm)"
  shows "composable_tm0 (fix_jumps (length tm div 2) tm)"
proof -
  from assms have "length (fix_jumps (length tm div 2) tm) ≥ 2 ∧
                   is_even (length (fix_jumps (length tm div 2) tm)) ∧ 
                   (∀x ∈ set (fix_jumps (length tm div 2) tm).
                      (snd x) ≤ length (fix_jumps (length tm div 2) tm) div 2 + 0 ∧ (snd x) ≥ 0)"
    by (rule composable_tm0_fix_jumps_pre)
  then show ?thesis by auto
qed


lemma fix_jumps_composable0_eq:
  assumes "composable_tm0 tm"
  shows "(fix_jumps (length tm div 2) tm) = tm"
proof -
  from assms have major: "∀(a, s) ∈ set tm. s ≤ length tm div 2" by auto
  then show "(fix_jumps (length tm div 2) tm) = tm"
    by  (induct rule: fix_jumps.induct)(auto)
qed

lemma composable_tm0_mk_composable0: "composable_tm0 (mk_composable0 tm)"
proof (rule mk_composable0.cases)
  assume "tm = []"
  then show "composable_tm0 (mk_composable0 tm)"
    by (auto simp add: composable_tm0_fix_jumps)
next
  fix i1
  assume "tm = [i1]"
  then show "composable_tm0 (mk_composable0 tm)"
    by (auto simp add: composable_tm0_fix_jumps)
next
  fix i1 i2 ins
  assume A: "tm = i1 # i2 # ins"
  then show "composable_tm0 (mk_composable0 tm)"
  proof (cases "is_even (2 + length ins)")
    case True
    then have "is_even (2 + length ins)" .
    then have "mk_composable0 (i1 # i2 # ins) = fix_jumps ((2 + length ins) div 2) (i1#i2#ins)"
      by auto
    also have "... = fix_jumps (length (i1#i2#ins) div 2) (i1#i2#ins)"
      by auto
    finally have "mk_composable0 (i1 # i2 # ins) = fix_jumps (length (i1#i2#ins) div 2) (i1#i2#ins)"
      by auto
    moreover have "composable_tm0 (fix_jumps (length (i1#i2#ins) div 2) (i1#i2#ins))"
    proof (rule composable_tm0_fix_jumps)
      show "2 ≤ length (i1 # i2 # ins)" by auto
    next
      from ‹is_even (2 + length ins)› show "is_even (length (i1 # i2 # ins))" 
        by (auto)
    qed
    ultimately show "composable_tm0 (mk_composable0 tm)" using A by auto
  next
    case False
    then have "(2 + length ins) mod 2 ≠ 0" .
    then have "mk_composable0 (i1 # i2 # ins) = fix_jumps (((2 + length ins) div 2) +1) ((i1#i2#ins)@[(Nop,0)])"
      by auto
    also have "... = fix_jumps ((length (i1#i2#ins) div 2) +1) ((i1#i2#ins)@[(Nop,0)])"
      by auto
    also have "... = fix_jumps (length (i1#i2#ins@[(Nop,0)]) div 2) ((i1#i2#ins)@[(Nop,0)])"
    proof -
      from ‹(2 + length ins) mod 2 ≠ 0›
      have "length ins mod 2 ≠ 0" by arith
      then have "length (i1 # i2 # ins ) mod 2  ≠ 0" by auto

      have "(length (i1 # i2 # ins ) div 2) + 1 = length (i1 # i2 # ins @ [(Nop, 0)]) div 2"
      proof -
        from ‹length (i1 # i2 # ins ) mod 2  ≠ 0›
        have "(length (i1 # i2 # ins ) div 2) + 1 = (length (i1 # i2 # ins) +1) div 2"
          by (rule odd_div2_plus_1_eq)
        also have "... = length (i1 # i2 # ins @ [(Nop, 0)]) div 2" by auto
        finally show ?thesis by auto
      qed

      then show "fix_jumps (length (i1 # i2 # ins) div 2 + 1) ((i1 # i2 # ins) @ [(Nop, 0)]) =
                 fix_jumps (length (i1 # i2 # ins @ [(Nop, 0)]) div 2) ((i1 # i2 # ins) @ [(Nop, 0)])"
        by auto
    qed
    finally have "mk_composable0 (i1 # i2 # ins) =
                   fix_jumps (length (i1 # i2 # ins @ [(Nop, 0)]) div 2) ((i1 # i2 # ins) @ [(Nop, 0)])"
      by auto

    moreover have "composable_tm0 (fix_jumps (length (i1 # i2 # ins @ [(Nop, 0)]) div 2) (i1 # i2 # ins @ [(Nop, 0)]))"
    proof (rule composable_tm0_fix_jumps)
      show " 2 ≤ length (i1 # i2 # ins @ [(Nop, 0)])" by auto
    next
      show "is_even (length (i1 # i2 # ins @ [(Nop, 0)]))"
      proof -
        from ‹(2 + length ins) mod 2 ≠ 0› have "length (i1 # i2 # ins) mod 2  ≠ 0" by auto
        then have "is_even (length (i1 # i2 # ins) +1)" by arith
        moreover have "length (i1 # i2 # ins) +1 = length (i1 # i2 # ins @ [(Nop, 0)])" by auto
        ultimately show "is_even (length (i1 # i2 # ins @ [(Nop, 0)]))" by auto
      qed
    qed
    ultimately show "composable_tm0 (mk_composable0 tm)" using A by auto
  qed
qed

subsection ‹Functions mk\_composable0 is the identity on composable Turing Machines›

lemma mk_composable0_eq:
  assumes "composable_tm0 tm"
  shows "mk_composable0 tm = tm"
proof -
  from assms have major: "length tm ≥ 2 ∧ is_even (length tm)" by auto
  show "mk_composable0 tm = tm"
  proof (rule mk_composable0.cases)
    assume "tm = []"
    with major have False by auto
    then show "mk_composable0 tm = tm" by auto
  next
    fix i1
    assume "tm = [i1]"
    with major have False by auto
    then show "mk_composable0 tm = tm" by auto
  next
    fix i1 i2 ins
    assume A: "tm = i1 # i2 # ins"
    then show " mk_composable0 tm = tm"
    proof (cases "is_even (2 + length ins)")
      case True
      then have "is_even (2 + length ins)" .
      then have "mk_composable0 (i1 # i2 # ins) = fix_jumps ((2 + length ins) div 2) (i1#i2#ins)"
        by auto
      also have "... = fix_jumps (length (i1#i2#ins) div 2) (i1#i2#ins)"
        by auto
      finally have "mk_composable0 (i1 # i2 # ins) = fix_jumps (length (i1#i2#ins) div 2) (i1#i2#ins)"
        by auto
      also have "fix_jumps (length (i1#i2#ins) div 2) (i1#i2#ins) = (i1#i2#ins)"
      proof (rule fix_jumps_composable0_eq)
        from assms and A show "composable_tm0 (i1 # i2 # ins)"
          by auto
      qed
      finally have "mk_composable0 (i1 # i2 # ins) = i1 # i2 # ins" by auto
      with A show "mk_composable0 tm = tm" by auto
    next
      case False
      then have "(2 + length ins) mod 2 ≠ 0" by auto
      then have "length (i1 # i2 # ins) mod 2 ≠ 0" by auto
      with A have "length tm   mod 2 ≠ 0" by auto
      with assms have False by auto
      then show ?thesis by auto
    qed
  qed
qed

(* ----------------------------------------------- *)
(* About the length of (mk_composable0 tm)                 *)
(* ----------------------------------------------- *)

subsection ‹About the length of mk\_composable0 tm›

lemma length_mk_composable0_nil: "length (mk_composable0 []) = 2"
  by auto

lemma length_mk_composable0_singleton: "length (mk_composable0 [i1]) = 2"
  by auto

lemma length_mk_composable0_gt2_even: "is_even (length (i1 # i2 # ins)) ⟹ length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins)"
proof -
  assume "is_even (length (i1 # i2 # ins))"
  then have "length (mk_composable0 (i1 # i2 # ins)) = length (fix_jumps ((length (i1 # i2 # ins)) div 2) (i1#i2#ins))" by auto
  also have "... = length (i1#i2#ins)" by (auto simp add: fix_jumps_len)
  finally show "length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins)" by auto
qed

lemma length_mk_composable0_gt2_odd: "¬is_even (length (i1 # i2 # ins)) ⟹ length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins)+1"
proof -
  assume "¬is_even (length (i1 # i2 # ins))"
  then have "length (mk_composable0 (i1 # i2 # ins)) = length (fix_jumps (((length (i1 # i2 # ins)) div 2)+1) ((i1#i2#ins)@[(Nop,0)]))" by auto
  also have "... = length ((i1#i2#ins)@[(Nop,0)])" by (auto simp add: fix_jumps_len)
  finally show "length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins) + 1" by auto
qed

lemma length_mk_composable0_even: "⟦0 < length tm ; is_even (length tm) ⟧ ⟹ length (mk_composable0 tm) = length tm"
proof (rule mk_composable0.cases[of tm])
  assume "0 < length tm"
    and  "is_even (length tm)"
    and "tm = []"
  then show ?thesis by auto
next
  fix i1
  assume "0 < length tm" and "is_even (length tm)" and "tm = [i1]"
  then show ?thesis by auto
next
  fix i1 i2 ins
  assume "0 < length tm" and "is_even (length tm)" and "tm = i1 # i2 # ins"
  then show ?thesis
  proof (cases "is_even (2 + length ins)")
    case True
    then have "is_even (2 + length ins)" .
    then have "mk_composable0 (i1 # i2 # ins) = fix_jumps ((2 + length ins) div 2) (i1#i2#ins)" by auto
    moreover have "length (fix_jumps ((2 + length ins) div 2) (i1#i2#ins)) = length (i1#i2#ins)"
      by (rule fix_jumps_len)
    ultimately have "length (mk_composable0 (i1 # i2 # ins)) =  length (i1#i2#ins)" by auto
    with ‹tm = i1 # i2 # ins› show ?thesis by auto
  next
    case False
    with ‹is_even (length tm)› and  ‹tm = i1 # i2 # ins› have False by auto
    then show ?thesis by auto
  qed
qed

lemma length_mk_composable0_odd: "⟦0 < length tm ; ¬is_even (length tm) ⟧ ⟹ length (mk_composable0 tm) = 1 + length tm"
proof (rule mk_composable0.cases[of tm])
  assume "0 < length tm"
    and  "¬ is_even (length tm)"
    and "tm = []"
  then show ?thesis by auto
next
  fix i1
  assume "0 < length tm" and "¬is_even (length tm)" and "tm = [i1]"
  then show ?thesis by auto
next
  fix i1 i2 ins
  assume "0 < length tm" and "¬is_even (length tm)" and "tm = i1 # i2 # ins"
  then show ?thesis
  proof (cases "is_even (2 + length ins)")
    case True
    with ‹¬is_even (length tm)› and ‹tm = i1 # i2 # ins› have False by auto
    then show ?thesis by auto
  next
    case False
    then have "¬is_even (2 + length ins)" by auto
    then have "mk_composable0 (i1 # i2 # ins) = fix_jumps (((2 + length ins) div 2)+1 ) ((i1#i2#ins)@[(Nop,0)])"
      by auto
    moreover have "length (fix_jumps ( ((2 + length ins) div 2)+1 ) ((i1#i2#ins)@[(Nop,0)])) = length ((i1#i2#ins)@[(Nop,0)])"
      by (rule fix_jumps_len)
    ultimately have "length (mk_composable0 (i1 # i2 # ins)) =  1 + length (i1#i2#ins)" by auto
    with ‹tm = i1 # i2 # ins› show ?thesis by auto
  qed
qed

lemma length_tm_le_mk_composable0: "length tm ≤ length (mk_composable0 tm)"
proof (cases "length tm")
  case 0
  then show ?thesis by auto
next
  case (Suc nat)
  then have A: "length tm = Suc nat" .
  show ?thesis
  proof (cases "is_even (length tm)")
    case True
    with A show ?thesis by (auto simp add: length_mk_composable0_even)
  next
    case False
    with A show ?thesis by (auto simp add: length_mk_composable0_odd)
  qed
qed


subsection ‹Properties of function fetch with respect to function mk\_composable0›

(* ----------------------------------------------- *)
(* Fetching instructions from  (mk_composable0 tm)         *)
(* ----------------------------------------------- *)

lemma fetch_mk_composable0_Bk_too_short_Suc:
  assumes "b = Bk" and "length tm ≤ 2*s"
  shows "fetch (mk_composable0 tm) (Suc s) b = (Nop, 0::nat)"
proof (rule mk_composable0.cases[of tm])
  assume "tm = []"
  then have "length (mk_composable0 tm) = 2" by auto
  with ‹tm = []› have "(mk_composable0 tm) = [(Nop,0),(Nop,0)]" by auto
  show "fetch (mk_composable0 tm) (Suc s) b = (Nop, 0)"
  proof (cases s)
    assume "s=0"
    with ‹length (mk_composable0 tm) = 2› 
    have "fetch (mk_composable0 tm) (Suc s) Bk = ((mk_composable0 tm) ! (2*s))"
      by (auto)
    also with ‹s=0› and  ‹(mk_composable0 tm) = [(Nop,0),(Nop,0)]› have "... = (Nop, 0::nat)" by auto
    finally have "fetch (mk_composable0 tm) (Suc s) Bk = (Nop, 0::nat)" by auto
    with ‹b = Bk› show ?thesis by auto
  next
    case (Suc nat)
    then have "s = Suc nat" .
    with ‹length (mk_composable0 tm) = 2› have "length (mk_composable0 tm) ≤ 2*s" by auto
    with ‹b = Bk› show ?thesis by (auto)
  qed
next
  fix i1
  assume "tm = [i1]"
  then have "mk_composable0 tm = fix_jumps 1 [i1,(Nop,0)]" by auto
  moreover have "length (fix_jumps 1 [i1,(Nop,0)]) = length [i1] +1" using fix_jumps_len by auto
  ultimately  have "length (mk_composable0 tm) = 2" using ‹tm = [i1]› by auto
  show "fetch (mk_composable0 tm) (Suc s) b = (Nop, 0)"
  proof (cases s)
    case 0
    with ‹tm = [i1]› and ‹length tm ≤ 2*s› have False by auto
    then show ?thesis by auto
  next
    case (Suc nat)
    then have "s = Suc nat" .
    with ‹length (mk_composable0 tm) = 2› have "length (mk_composable0 tm) ≤ 2*s" by arith
    with ‹b = Bk› show ?thesis by (auto)
  qed
next
  fix i1 i2 ins
  assume "tm = i1 # i2 # ins"
  show "fetch (mk_composable0 tm) (Suc s) b = (Nop, 0)"
  proof (cases "is_even (2 + length ins)")
    case True
    then have "is_even (2 + length ins)" .
    with ‹tm = i1 # i2 # ins› have "mk_composable0 tm = fix_jumps ((2 + length ins) div 2) tm" by auto
    moreover have "length(fix_jumps ((2 + length ins) div 2) tm) = length tm" using fix_jumps_len by auto
    ultimately have "length (mk_composable0 tm) = length tm" by auto  
    with ‹length tm ≤ 2*s› have "length (mk_composable0 tm) ≤ 2*s" by auto
    with ‹b = Bk› show ?thesis by auto
  next
    case False
    then have "¬is_even (2 + length ins)" .
    with ‹tm = i1 # i2 # ins›
    have "mk_composable0 tm = fix_jumps (((2 + length ins) div 2)+1) (tm@[(Nop,0)])" by auto
    moreover
    have "length(fix_jumps (((2 + length ins) div 2)+1) (tm@[(Nop,0)])) = length (tm@[(Nop,0)])" using fix_jumps_len by auto
    ultimately have "length (mk_composable0 tm) = length tm +1" by auto  
    moreover from ‹¬is_even (2 + length ins)› and  ‹tm = i1 # i2 # ins› have "¬is_even (length tm)" by auto
    with ‹length tm ≤ 2*s› have "length tm +1 ≤ 2*s" by arith
    with ‹length (mk_composable0 tm) = length tm +1› have "length (mk_composable0 tm) ≤ 2*s" by auto
    with ‹b = Bk› show ?thesis by auto
  qed
qed


lemma fetch_mk_composable0_Oc_too_short_Suc:
  assumes "b = Oc" and "length tm ≤ 2*s+1"
  shows "fetch (mk_composable0 tm) (Suc s) b = (Nop, 0::nat)"
proof (rule mk_composable0.cases[of tm])
  assume "tm = []"
  then have "length (mk_composable0 tm) = 2" by auto
  with ‹tm = []› have "(mk_composable0 tm) = [(Nop,0),(Nop,0)]" by auto
  show "fetch (mk_composable0 tm) (Suc s) b = (Nop, 0)"
  proof (cases s)
    assume "s=0"
    with ‹length (mk_composable0 tm) = 2› 
    have "fetch (mk_composable0 tm) (Suc s) Oc = ((mk_composable0 tm) ! (2*s+1))"
      by (auto)
    also with ‹s=0› and  ‹(mk_composable0 tm) = [(Nop,0),(Nop,0)]› have "... = (Nop, 0::nat)" by auto
    finally have "fetch (mk_composable0 tm) (Suc s) Oc = (Nop, 0::nat)" by auto
    with ‹b = Oc› show ?thesis by auto
  next
    case (Suc nat)
    then have "s = Suc nat" .
    with ‹length (mk_composable0 tm) = 2› have "length (mk_composable0 tm) ≤ 2*s" by auto
    with ‹b = Oc› show ?thesis by (auto)
  qed
next
  fix i1
  assume "tm = [i1]"
  then have "mk_composable0 tm = fix_jumps 1 [i1,(Nop,0)]" by auto
  moreover have "length (fix_jumps 1 [i1,(Nop,0)]) = length [i1] +1" using fix_jumps_len by auto
  ultimately  have "length (mk_composable0 tm) = 2" using ‹tm = [i1]› by auto
  show "fetch (mk_composable0 tm) (Suc s) b = (Nop, 0)"
  proof (cases s)
    case 0
    then have "s=0" .
    with ‹length (mk_composable0 tm) = 2› have "fetch (mk_composable0 tm) (Suc s) Oc = ((mk_composable0 tm) ! 1)"
      by (auto)
    also with ‹mk_composable0 tm = fix_jumps 1 [i1,(Nop,0)]› have "... = ((fix_jumps 1 [i1,(Nop,0)]) ! 1)"
      by auto
    also have "... = (Nop, 0)" by (cases "(snd i1) ≤ 1")(auto)
    finally have "fetch (mk_composable0 tm) (Suc s) Oc = (Nop, 0)" by auto
    with ‹b = Oc› show ?thesis by auto
  next
    case (Suc nat)
    then have "s = Suc nat" .
    with ‹length (mk_composable0 tm) = 2› have "length (mk_composable0 tm) ≤ 2*s+1" by arith
    with ‹b = Oc› show ?thesis by (auto)
  qed
next
  fix i1 i2 ins
  assume "tm = i1 # i2 # ins"
  show "fetch (mk_composable0 tm) (Suc s) b = (Nop, 0)"
  proof (cases "is_even (2 + length ins)")
    case True
    then have "is_even (2 + length ins)" .
    with ‹tm = i1 # i2 # ins› have "mk_composable0 tm = fix_jumps ((2 + length ins) div 2) tm" by auto
    moreover have "length(fix_jumps ((2 + length ins) div 2) tm) = length tm" using fix_jumps_len by auto
    ultimately have "length (mk_composable0 tm) = length tm" by auto  
    with ‹length tm ≤ 2*s+1› have "length (mk_composable0 tm) ≤ 2*s+1" by auto
    with ‹b = Oc› show ?thesis by auto
  next
    case False
    then have "¬is_even (2 + length ins)" .
    with ‹tm = i1 # i2 # ins›
    have F1: "mk_composable0 tm = fix_jumps (((2 + length ins) div 2)+1) (tm@[(Nop,0)])" by auto
    moreover
    have "length(fix_jumps (((2 + length ins) div 2)+1) (tm@[(Nop,0)])) = length (tm@[(Nop,0)])"
      using fix_jumps_len by auto
    ultimately have "length (mk_composable0 tm) = length tm +1" by auto

    moreover from ‹¬is_even (2 + length ins)› and  ‹tm = i1 # i2 # ins›
    have "¬is_even (length tm)" by auto

    from ‹length tm ≤ 2*s+1› have  "(length tm) = (2*s+1) ∨ (length tm) < 2*s+1" by auto
    then show ?thesis
    proof
      assume "length tm = 2 * s + 1"
      from ‹length tm = 2 * s + 1› and ‹length (mk_composable0 tm) = length tm +1› have "length (mk_composable0 tm) = 2*s + 2" by auto
      from ‹length tm = 2 * s + 1› and ‹length (mk_composable0 tm) = length tm +1› have "length (mk_composable0 tm) > 2*s+1" by arith
      with ‹b = Oc› have "fetch (mk_composable0 tm) (Suc s) b = ((mk_composable0 tm) ! (2*s+1))" by (auto )
      also with ‹length (mk_composable0 tm) = 2 * s + 2› have "... = (mk_composable0 tm) ! (length (mk_composable0 tm)-1)" by auto
      also with F1 have "... = (fix_jumps (((2 + length ins) div 2)+1) (tm@[(Nop,0)])) ! (length (mk_composable0 tm)-1)" by auto
      also have "... = (Nop, 0)"
      proof (rule fix_jumps_nth_no_fix)
        show "snd (Nop, 0) ≤ (2 + length ins) div 2 + 1" by auto
      next
        from ‹length (mk_composable0 tm) = length tm +1› show "length (mk_composable0 tm) - 1 < length (tm @ [(Nop, 0)])" by auto
      next 
        from  ‹length (mk_composable0 tm) = length tm +1› show "(tm @ [(Nop, 0)]) ! (length (mk_composable0 tm) - 1) = (Nop, 0)" by auto
      qed
      finally show "fetch (mk_composable0 tm) (Suc s) b =  (Nop, 0)" by auto
    next
      assume "length tm < 2 * s + 1 "
      with ‹¬is_even (length tm)› have "length tm +1 ≤ 2 * s + 1" by auto
      with ‹length (mk_composable0 tm) = length tm +1› have "length (mk_composable0 tm)  ≤ 2 * s + 1" by auto
      with ‹b = Oc› show "fetch (mk_composable0 tm) (Suc s) b = (Nop, 0::nat)"
        by (auto)
    qed
  qed
qed

lemma nth_append': "n < length xs ⟹ (xs @ ys) ! n = xs ! n" by (auto simp add: nth_append)

lemma fetch_mk_composable0_Bk_Suc_no_fix:
  assumes "b = Bk"
    and "2*s < length tm"
    and "fetch tm (Suc s) b = (a, s')"
    and "s' ≤ length (mk_composable0 tm) div 2"
  shows "fetch (mk_composable0 tm) (Suc s) b = fetch tm (Suc s) b"
proof (rule mk_composable0.cases[of tm])
  assume "tm = []"
  with ‹length tm > 2*s› show ?thesis by auto
next
  fix i1
  assume "tm = [i1]"
  have "fetch (mk_composable0 tm) (Suc s) b = (mk_composable0 tm)!(2*s)"
    using ‹tm = [i1]› assms by auto
  also have "(mk_composable0 tm)!(2*s) = (a, s')"
  proof -
    from ‹tm = [i1]› have "length (mk_composable0 tm) = 2" by auto
    have "(mk_composable0 [i1])!(2*s) = (fix_jumps 1 [i1,(Nop,0)])!(2*s)" by auto
    also have "... = (a, s')"
    proof (rule fix_jumps_nth_no_fix)
      from assms and  ‹tm = [i1]› show "2 * s < length [i1, (Nop, 0)]" by auto
    next
      from assms and  ‹tm = [i1]› show "[i1, (Nop, 0)] ! (2 * s) = (a, s')" by auto
    next
      from assms and  ‹tm = [i1]› and ‹length (mk_composable0 tm) = 2› show "snd (a, s') ≤ 1" by auto
    qed
    finally have "(mk_composable0 [i1])!(2*s) = (a, s')" by auto
    with  ‹tm = [i1]› show ?thesis by auto
  qed
  finally have "fetch (mk_composable0 tm) (Suc s) b = (a, s')" by auto
  with assms show ?thesis by auto
next
  fix i1 i2 ins
  assume "tm = i1 # i2 # ins"
  have "fetch (mk_composable0 tm) (Suc s) b = (mk_composable0 tm)!(2*s)"
  proof -
    have "¬ length (mk_composable0 tm) ≤ 2 * Suc s - 2"
      by (metis (no_types) add_diff_cancel_left' assms(2) le_trans length_tm_le_mk_composable0 mult_Suc_right not_less)
    then show ?thesis
      by (simp add: assms(1))
  qed
    
    also have "(mk_composable0 tm)!(2*s) = (a, s')"
  proof (cases "is_even (length tm)")
    case True
    then have "is_even (length tm)" .
    with ‹tm = i1 # i2 # ins› have  "is_even (length (i1 # i2 # ins))" by auto
    then have "length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins)" by (rule length_mk_composable0_gt2_even)

    from ‹is_even (length (i1 # i2 # ins))›
    have "(mk_composable0 (i1 # i2 # ins))!(2*s) = (fix_jumps ((length (i1 # i2 # ins)) div 2) (i1#i2#ins))!(2*s)" by auto
    also have "... = (a, s')"
    proof (rule fix_jumps_nth_no_fix)
      from assms and  ‹tm = i1 # i2 # ins› show "2 * s < length (i1 # i2 # ins)" by auto
    next
      from assms and  ‹tm = i1 # i2 # ins› show "(i1 # i2 # ins) ! (2 * s) = (a, s')" by auto
    next
      from assms and  ‹tm = i1 # i2 # ins› and ‹length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins)›
      show "snd (a, s') ≤ length (i1 # i2 # ins) div 2" by auto
    qed
    finally have "(mk_composable0 (i1 # i2 # ins))!(2*s) = (a, s')" by auto
    with ‹tm = i1 # i2 # ins› show ?thesis by auto
  next
    case False
    then have "¬is_even (length tm)" .
    with ‹tm = i1 # i2 # ins› have  "¬is_even (length (i1 # i2 # ins))" by auto
    then have "length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins) +1" by (rule length_mk_composable0_gt2_odd)

    from ‹¬is_even (length (i1 # i2 # ins))›
    have "(mk_composable0 (i1 # i2 # ins))!(2*s) = (fix_jumps (((length (i1 # i2 # ins)) div 2)+1) ((i1#i2#ins)@[(Nop,0)]))!(2*s)" by auto
    also have "... = (a, s')"
    proof (rule fix_jumps_nth_no_fix)
      from assms and ‹tm = i1 # i2 # ins› show "2 * s < length ((i1 # i2 # ins) @ [(Nop, 0)])" by auto
    next
      have "((i1 # i2 # ins)@ [(Nop, 0)]) ! (2 * s) = ((i1 # i2 # ins)) ! (2 * s)"
      proof (rule nth_append')
        from assms and ‹tm = i1 # i2 # ins› show "2 * s < length (i1 # i2 # ins)" by auto
      qed
      also from assms and ‹tm = i1 # i2 # ins› have "((i1 # i2 # ins)) ! (2 * s) = (a, s')" by auto
      finally show "((i1 # i2 # ins)@ [(Nop, 0)]) ! (2 * s) = (a, s')" by auto
    next
      from assms and  ‹tm = i1 # i2 # ins› and ‹length (mk_composable0 (i1 # i2 # ins)) = length ((i1#i2#ins)) + 1›
      show "snd (a, s') ≤ length (i1 # i2 # ins) div 2 + 1" by auto 
    qed
    finally have "(mk_composable0 (i1 # i2 # ins))!(2*s) = (a, s')" by auto
    with ‹tm = i1 # i2 # ins› show ?thesis by auto
  qed
  finally have "fetch (mk_composable0 tm) (Suc s) b = (a, s')" by auto
  with assms show ?thesis by auto
qed

lemma fetch_mk_composable0_Bk_Suc_fix:
assumes "b = Bk"
    and "2*s < length tm"
    and "fetch tm (Suc s) b = (a, s')"
    and "length (mk_composable0 tm) div 2 < s'"
shows "fetch (mk_composable0 tm) (Suc s) b = (a, 0)"
proof (rule mk_composable0.cases[of tm])
  assume "tm = []"
  with ‹length tm > 2*s› show ?thesis by auto
next
  fix i1
  assume "tm = [i1]"
  have "fetch (mk_composable0 tm) (Suc s) b = (mk_composable0 tm)!(2*s)"
    using ‹tm = [i1]› assms(1) assms(2) by auto
  also have "(mk_composable0 tm)!(2*s) = (a, 0)"
  proof -
    from ‹tm = [i1]› have "length (mk_composable0 tm) = 2" by auto
    have "(mk_composable0 [i1])!(2*s) = (fix_jumps 1 [i1,(Nop,0)])!(2*s)" by auto
    also have "... = (fst(a,s'), 0)"
    proof (rule fix_jumps_nth_fix)
      from assms and  ‹tm = [i1]› show "2 * s < length [i1, (Nop, 0)]" by auto
    next
      from assms and  ‹tm = [i1]› show "[i1, (Nop, 0)] ! (2 * s) = (a, s')" by auto
    next
      from assms and  ‹tm = [i1]› and ‹length (mk_composable0 tm) = 2› show "¬snd (a, s') ≤ 1" by auto
    qed
    finally have "(mk_composable0 [i1])!(2*s) = (a, 0)" by auto
    with  ‹tm = [i1]› show ?thesis by auto
  qed
  finally have "fetch (mk_composable0 tm) (Suc s) b = (a, 0)" by auto
  with assms show ?thesis by auto
next
  fix i1 i2 ins
  assume "tm = i1 # i2 # ins"
  from assms have "fetch tm (Suc s) b = (tm ! (2*s))"
    by (auto)
  have "fetch (mk_composable0 tm) (Suc s) b = (mk_composable0 tm)!(2*s)"
    using assms(1) assms(3) assms(4) le_trans length_tm_le_mk_composable0
    by fastforce
  also have "(mk_composable0 tm)!(2*s) = (a, 0)"
  proof (cases "is_even (length tm)")
    case True
    then have "is_even (length tm)" .
    with ‹tm = i1 # i2 # ins› have  "is_even (length (i1 # i2 # ins))" by auto
    then have "length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins)" by (rule length_mk_composable0_gt2_even)

    from ‹is_even (length (i1 # i2 # ins))›
    have "(mk_composable0 (i1 # i2 # ins))!(2*s) = (fix_jumps ((length (i1 # i2 # ins)) div 2) (i1#i2#ins))!(2*s)" by auto
    also have "... = (fst(a,s'),0)"

    proof (rule fix_jumps_nth_fix)
      from assms and  ‹tm = i1 # i2 # ins› show "2 * s < length (i1 # i2 # ins)" by auto
    next
      from assms and  ‹tm = i1 # i2 # ins› show "(i1 # i2 # ins) ! (2 * s) = (a, s')" by auto
    next
      from assms and  ‹tm = i1 # i2 # ins› and ‹length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins)›
      show "¬snd (a, s') ≤ length (i1 # i2 # ins) div 2" by auto
    qed
    finally have "(mk_composable0 (i1 # i2 # ins))!(2*s) = (fst(a,s'),0)" by auto
    then have "(mk_composable0 (i1 # i2 # ins))!(2*s) = (a,0)" by auto
    with ‹tm = i1 # i2 # ins› show ?thesis by auto
  next
    case False
    then have "¬is_even (length tm)" .
    with ‹tm = i1 # i2 # ins› have  "¬is_even (length (i1 # i2 # ins))" by auto
    then have "length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins) +1" by (rule length_mk_composable0_gt2_odd)
    from ‹¬is_even (length (i1 # i2 # ins))›
    have "(mk_composable0 (i1 # i2 # ins))!(2*s) = (fix_jumps (((length (i1 # i2 # ins)) div 2)+1) ((i1#i2#ins)@[(Nop,0)]))!(2*s)" by auto
    also have "... = (fst(a,s'), 0)"
    proof (rule fix_jumps_nth_fix)
      from assms and ‹tm = i1 # i2 # ins› show "2 * s < length ((i1 # i2 # ins) @ [(Nop, 0)])" by auto
    next
      have "((i1 # i2 # ins)@ [(Nop, 0)]) ! (2 * s) = ((i1 # i2 # ins)) ! (2 * s)"
      proof (rule nth_append')
        from assms and ‹tm = i1 # i2 # ins› show "2 * s < length (i1 # i2 # ins)" by auto
      qed
      also from assms and ‹tm = i1 # i2 # ins› have "((i1 # i2 # ins)) ! (2 * s) = (a, s')" by auto
      finally show "((i1 # i2 # ins)@ [(Nop, 0)]) ! (2 * s) = (a, s')" by auto
    next
      from assms and ‹tm = i1 # i2 # ins› and ‹length (mk_composable0 (i1 # i2 # ins)) = length ((i1#i2#ins)) + 1›
      have "s' > (length (i1 # i2 # ins) + 1) div 2" by auto
      with ‹¬is_even (length (i1 # i2 # ins))› have "s' > length (i1 # i2 # ins) div 2 + 1" by arith
      then show "¬ snd (a, s') ≤ length (i1 # i2 # ins) div 2 + 1" by auto 
    qed
    finally have "(mk_composable0 (i1 # i2 # ins))!(2*s) = (a, 0)" by auto
    with ‹tm = i1 # i2 # ins› show ?thesis by auto
  qed
  finally have "fetch (mk_composable0 tm) (Suc s) b = (a, 0)" by auto
  with assms show ?thesis by auto
qed

lemma fetch_mk_composable0_Oc_Suc_no_fix:
  assumes "b = Oc"
    and "2*s+1 < length tm"
    and "fetch tm (Suc s) b = (a, s')"

    and "s' ≤ length (mk_composable0 tm) div 2"
  shows "fetch (mk_composable0 tm) (Suc s) b = fetch tm (Suc s) b"
proof (rule mk_composable0.cases[of tm])
  assume "tm = []"
  with ‹2*s+1 < length tm› show ?thesis by auto
next
  fix i1
  assume "tm = [i1]"
  have "fetch (mk_composable0 tm) (Suc s) b = (mk_composable0 tm)!(2*s+1)"
    using ‹tm = [i1]› assms(2) by auto
  also have "(mk_composable0 tm)!(2*s+1) = (a, s')"
  proof -
    from ‹tm = [i1]› have "length (mk_composable0 tm) = 2" by auto
    have "(mk_composable0 [i1])!(2*s+1) = (fix_jumps 1 [i1,(Nop,0)])!(2*s+1)" by auto
    also have "... = (a, s')"
    proof (rule fix_jumps_nth_no_fix)
      from assms and  ‹tm = [i1]› show "2 * s  +1 < length [i1, (Nop, 0)]" by auto
    next
      from assms and  ‹tm = [i1]› show "[i1, (Nop, 0)] ! (2 * s +1) = (a, s')" by auto
    next
      from assms and  ‹tm = [i1]› and ‹length (mk_composable0 tm) = 2› show "snd (a, s') ≤ 1" by auto
    qed
    finally have "(mk_composable0 [i1])!(2*s+1) = (a, s')" by auto
    with  ‹tm = [i1]› show ?thesis by auto
  qed
  finally have "fetch (mk_composable0 tm) (Suc s) b = (a, s')" by auto
  with assms show ?thesis by auto
next
  fix i1 i2 ins
  assume "tm = i1 # i2 # ins"
  have "fetch (mk_composable0 tm) (Suc s) b = (mk_composable0 tm)!(2*s+1)"
  proof -
    have "¬ length (mk_composable0 tm) ≤ 2 * s + 1"
      by (meson assms(2) le_trans length_tm_le_mk_composable0 not_less)
    then show ?thesis
      by (simp add: assms(1))
  qed
  also have "(mk_composable0 tm)!(2*s+1) = (a, s')"
  proof (cases "is_even (length tm)")
    case True
    then have "is_even (length tm)" .
    with ‹tm = i1 # i2 # ins› have  "is_even (length (i1 # i2 # ins))" by auto
    then have "length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins)" by (rule length_mk_composable0_gt2_even)

    from ‹is_even (length (i1 # i2 # ins))›
    have "(mk_composable0 (i1 # i2 # ins))!(2*s+1) = (fix_jumps ((length (i1 # i2 # ins)) div 2) (i1#i2#ins))!(2*s+1)" by auto
    also have "... = (a, s')"
    proof (rule fix_jumps_nth_no_fix)
      from assms and  ‹tm = i1 # i2 # ins› show "2 * s+1 < length (i1 # i2 # ins)" by auto
    next
      from assms and  ‹tm = i1 # i2 # ins› show "(i1 # i2 # ins) ! (2 * s+1) = (a, s')" by auto
    next
      from assms and  ‹tm = i1 # i2 # ins› and ‹length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins)›
      show "snd (a, s') ≤ length (i1 # i2 # ins) div 2" by auto
    qed
    finally have "(mk_composable0 (i1 # i2 # ins))!(2*s+1) = (a, s')" by auto
    with ‹tm = i1 # i2 # ins› show ?thesis by auto
  next
    case False
    then have "¬is_even (length tm)" .
    with ‹tm = i1 # i2 # ins› have  "¬is_even (length (i1 # i2 # ins))" by auto
    then have "length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins) +1" by (rule length_mk_composable0_gt2_odd)

    from ‹¬is_even (length (i1 # i2 # ins))›
    have "(mk_composable0 (i1 # i2 # ins))!(2*s+1) = (fix_jumps (((length (i1 # i2 # ins)) div 2)+1) ((i1#i2#ins)@[(Nop,0)]))!(2*s+1)" by auto
    also have "... = (a, s')"
    proof (rule fix_jumps_nth_no_fix)
      from assms and ‹tm = i1 # i2 # ins› show "2 * s +1< length ((i1 # i2 # ins) @ [(Nop, 0)])" by auto
    next
      have "((i1 # i2 # ins)@ [(Nop, 0)]) ! (2 * s+1) = ((i1 # i2 # ins)) ! (2 * s+1)"
      proof (rule nth_append')
        from assms and ‹tm = i1 # i2 # ins› show "2 * s+1 < length (i1 # i2 # ins)" by auto
      qed
      also from assms and ‹tm = i1 # i2 # ins› have "((i1 # i2 # ins)) ! (2 * s+1) = (a, s')" by auto
      finally show "((i1 # i2 # ins)@ [(Nop, 0)]) ! (2 * s+1) = (a, s')" by auto
    next
      from assms and  ‹tm = i1 # i2 # ins› and ‹length (mk_composable0 (i1 # i2 # ins)) = length ((i1#i2#ins)) + 1›
      show "snd (a, s') ≤ length (i1 # i2 # ins) div 2 + 1" by auto 
    qed
    finally have "(mk_composable0 (i1 # i2 # ins))!(2*s+1) = (a, s')" by auto
    with ‹tm = i1 # i2 # ins› show ?thesis by auto
  qed
  finally have "fetch (mk_composable0 tm) (Suc s) b = (a, s')" by auto
  with assms show ?thesis by auto
qed


lemma fetch_mk_composable0_Oc_Suc_fix:
assumes "b = Oc"
    and "2*s+1 < length tm"
    and "fetch tm (Suc s) b = (a, s')"

    and "length (mk_composable0 tm) div 2 < s'"
shows "fetch (mk_composable0 tm) (Suc s) b = (a, 0)"
proof (rule mk_composable0.cases[of tm])
  assume "tm = []"
  with ‹length tm > 2*s+1› show ?thesis by auto
next
  fix i1
  assume "tm = [i1]"
  have "fetch (mk_composable0 tm) (Suc s) b = (mk_composable0 tm)!(2*s+1)"
    using ‹tm = [i1]› assms(2) by auto
  also have "(mk_composable0 tm)!(2*s+1) = (a, 0)"
  proof -
    from ‹tm = [i1]› have "length (mk_composable0 tm) = 2" by auto
    have "(mk_composable0 [i1])!(2*s+1) = (fix_jumps 1 [i1,(Nop,0)])!(2*s+1)" by auto
    also have "... = (fst(a,s'), 0)"
    proof (rule fix_jumps_nth_fix)
      from assms and  ‹tm = [i1]› show "2 * s+1 < length [i1, (Nop, 0)]" by auto
    next
      from assms and  ‹tm = [i1]› show "[i1, (Nop, 0)] ! (2 * s+1) = (a, s')" by auto
    next
      from assms and  ‹tm = [i1]› and ‹length (mk_composable0 tm) = 2› show "¬snd (a, s') ≤ 1" by auto
    qed
    finally have "(mk_composable0 [i1])!(2*s+1) = (a, 0)" by auto
    with  ‹tm = [i1]› show ?thesis by auto
  qed
  finally have "fetch (mk_composable0 tm) (Suc s) b = (a, 0)" by auto
  with assms show ?thesis by auto
next
  fix i1 i2 ins
  assume "tm = i1 # i2 # ins"
  from assms have "fetch tm (Suc s) b = (tm ! (2*s+1))"
    by (auto)
  have "fetch (mk_composable0 tm) (Suc s) b = (mk_composable0 tm)!(2*s+1)"
  proof -
    have "¬ length (mk_composable0 tm) ≤ 2 * s + 1"
      by (meson assms(2) le_trans length_tm_le_mk_composable0 not_less)
    then show ?thesis
      by (simp add: assms(1))
  qed
  also have "(mk_composable0 tm)!(2*s+1) = (a, 0)"
  proof (cases "is_even (length tm)")
    case True
    then have "is_even (length tm)" .
    with ‹tm = i1 # i2 # ins› have  "is_even (length (i1 # i2 # ins))" by auto
    then have "length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins)" by (rule length_mk_composable0_gt2_even)

    from ‹is_even (length (i1 # i2 # ins))›
    have "(mk_composable0 (i1 # i2 # ins))!(2*s+1) = (fix_jumps ((length (i1 # i2 # ins)) div 2) (i1#i2#ins))!(2*s+1)" by auto
    also have "... = (fst(a,s'),0)"

    proof (rule fix_jumps_nth_fix)
      from assms and  ‹tm = i1 # i2 # ins› show "2 * s +1 < length (i1 # i2 # ins)" by auto
    next
      from assms and  ‹tm = i1 # i2 # ins› show "(i1 # i2 # ins) ! (2 * s +1) = (a, s')" by auto
    next
      from assms and  ‹tm = i1 # i2 # ins› and ‹length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins)›
      show "¬snd (a, s') ≤ length (i1 # i2 # ins) div 2" by auto
    qed
    finally have "(mk_composable0 (i1 # i2 # ins))!(2*s+1) = (fst(a,s'),0)" by auto
    then have "(mk_composable0 (i1 # i2 # ins))!(2*s+1) = (a,0)" by auto
    with ‹tm = i1 # i2 # ins› show ?thesis by auto
  next
    case False
    then have "¬is_even (length tm)" .
    with ‹tm = i1 # i2 # ins› have  "¬is_even (length (i1 # i2 # ins))" by auto
    then have "length (mk_composable0 (i1 # i2 # ins)) = length (i1#i2#ins) +1" by (rule length_mk_composable0_gt2_odd)
    from ‹¬is_even (length (i1 # i2 # ins))›
    have "(mk_composable0 (i1 # i2 # ins))!(2*s+1) = (fix_jumps (((length (i1 # i2 # ins)) div 2)+1) ((i1#i2#ins)@[(Nop,0)]))!(2*s+1)" by auto
    also have "... = (fst(a,s'), 0)"
    proof (rule fix_jumps_nth_fix)
      from assms and ‹tm = i1 # i2 # ins› show "2 * s+1 < length ((i1 # i2 # ins) @ [(Nop, 0)])" by auto
    next
      have "((i1 # i2 # ins)@ [(Nop, 0)]) ! (2 * s +1) = ((i1 # i2 # ins)) ! (2 * s +1)"
      proof (rule nth_append')
        from assms and ‹tm = i1 # i2 # ins› show "2 * s +1 < length (i1 # i2 # ins)" by auto
      qed
      also from assms and ‹tm = i1 # i2 # ins› have "((i1 # i2 # ins)) ! (2 * s +1) = (a, s')" by auto
      finally show "((i1 # i2 # ins)@ [(Nop, 0)]) ! (2 * s +1) = (a, s')" by auto
    next
      from assms and ‹tm = i1 # i2 # ins› and ‹length (mk_composable0 (i1 # i2 # ins)) = length ((i1#i2#ins)) + 1›
      have "s' > (length (i1 # i2 # ins) + 1) div 2" by auto
      with ‹¬is_even (length (i1 # i2 # ins))› have "s' > length (i1 # i2 # ins) div 2 + 1" by arith
      then show "¬ snd (a, s') ≤ length (i1 # i2 # ins) div 2 + 1" by auto 
    qed
    finally have "(mk_composable0 (i1 # i2 # ins))!(2*s+1) = (a, 0)" by auto
    with ‹tm = i1 # i2 # ins› show ?thesis by auto
  qed
  finally have "fetch (mk_composable0 tm) (Suc s) b = (a, 0)" by auto
  with assms show ?thesis by auto
qed


subsection ‹Properties of function step0 with respect to function mk\_composable0›

lemma length_mk_composable0_div2_lt_imp_length_tm_le_times2:
  assumes "length (mk_composable0 tm) div 2 < s'"
    and "s' = Suc s2"
  shows "length tm ≤ 2 * s2"
proof (cases "length tm")
  case 0
  then show ?thesis by auto
next
  case (Suc nat)
  then have "length tm = Suc nat" .
  then show ?thesis
  proof (cases  "is_even (length tm)")
    case True
    then have "is_even (length tm)" .

    from  ‹length (mk_composable0 tm) div 2 < s'›
      and ‹s' = Suc s2› have "length (mk_composable0 tm) div 2 < Suc s2" by auto
    moreover from ‹is_even (length tm)› and ‹length tm = Suc nat›
    have "length (mk_composable0 tm) = length tm"
      by (auto simp add: length_mk_composable0_even)
    ultimately have "length tm div 2 < Suc s2" by auto
    with ‹is_even (length tm)› show ?thesis by (auto simp add: even_le_div2_imp_le_times_2)
  next
    case False
    then have "¬ is_even (length tm)" .
    from  ‹length (mk_composable0 tm) div 2 < s'› and ‹s' = Suc s2›
    have "length (mk_composable0 tm) div 2 < Suc s2" by auto
    moreover from ‹¬is_even (length tm)›
      and ‹length tm = Suc nat› have "length (mk_composable0 tm) = length tm +1"
      by (auto simp add: length_mk_composable0_odd)
    ultimately have "(length tm +1) div 2 < Suc s2" by auto
    with ‹¬is_even (length tm)› show ?thesis by (auto simp add: odd_le_div2_imp_le_times_2)
  qed
qed

lemma jump_out_of_pgm_is_final_next_step:
  assumes "step0 (s, l, r) tm = (s', update a1 (l, r))"
    and "s' = Suc s2" and "length (mk_composable0 tm) div 2 < s'"
  shows "step0 (step0 (s, l, r) tm) tm = (0, snd (step0 (s, l, r) tm))"
proof -
  from ‹length (mk_composable0 tm) div 2 < s'› and ‹s' = Suc s2› have "length tm ≤ 2 * s2"
    by (rule length_mk_composable0_div2_lt_imp_length_tm_le_times2)
  with assms have  "step0 (step0 (s, l, r) tm) tm = step0 (s', update a1 (l, r)) tm" by auto
  also have "... = (0::nat, update a1 (l, r))"
  proof (cases "update a1 (l, r)")
    fix l2 r2
    assume "update a1 (l, r) = (l2, r2)"
    then show ?thesis 
    proof (cases "read r2")
      case Bk
      then have "read r2 = Bk" .
      moreover with ‹length tm ≤ 2 * s2› and ‹s' = Suc s2› fetch.simps
      have "fetch tm s' Bk = (Nop, 0::nat)" by auto
      ultimately show ?thesis by (auto simp add: ‹update a1 (l, r) = (l2, r2)› )
    next
      case Oc
      then have "read r2 = Oc" .
      moreover with ‹length tm ≤ 2 * s2› and ‹s' = Suc s2› fetch.simps
      have "fetch tm s' Oc = (Nop, 0::nat)" by auto
      ultimately show ?thesis by (auto simp add: ‹update a1 (l, r) = (l2, r2)› )
    qed
  qed
  finally have "step0 (step0 (s, l, r) tm) tm = (0, update a1 (l, r)) " by auto

  with ‹step0 (s, l, r) tm = (s', update a1 (l, r))› show ?thesis by auto
qed



lemma step0_mk_composable0_after_one_step:
  assumes "step0 (s, (l, r)) tm ≠ step0 (s, l, r) (mk_composable0 tm)"
  shows "step0 (step0 (s, (l, r)) tm) tm = (0, snd((step0 (s, (l, r)) tm))) ∧
         step0 (s, l, r) (mk_composable0 tm)     = (0, snd((step0 (s, (l, r)) tm)))"
proof (cases "(read r)"; cases s)
  assume "read r = Bk" and "s = 0"
  show "step0 (step0 (s, l, r) tm) tm = (0, snd (step0 (s, l, r) tm)) ∧ step0 (s, l, r) (mk_composable0 tm) = (0, snd (step0 (s, l, r) tm))"
  proof (cases "length tm ≤ 2*s")
    case True
    with ‹s = 0› show ?thesis by auto
  next  
    case False
    then have "2 * s < length tm" by auto
    with ‹s = 0› show ?thesis by auto
  qed
next
  assume "read r = Oc" and "s = 0"
  show "step0 (step0 (s, l, r) tm) tm = (0, snd (step0 (s, l, r) tm)) ∧ step0 (s, l, r) (mk_composable0 tm) = (0, snd (step0 (s, l, r) tm))"
  proof (cases "length tm ≤ 2*s")
    case True
    then have "length tm ≤ 2 * s" .
    with ‹s = 0› show ?thesis by auto
  next  
    case False
    then have "2 * s < length tm" by auto
    with ‹s = 0› show ?thesis by auto
  qed
next
  fix s1
  assume "read r = Bk" and "s = Suc s1"
  show ?thesis
  proof (cases "length tm ≤ 2*s1")  (* both programs will fetch a Nop *)
    assume "length tm ≤ 2 * s1"
    with ‹read r = Bk› and ‹s = Suc s1› have "fetch tm (Suc s1) (read r) = (Nop, 0::nat)"
      by (auto)
    moreover have "fetch (mk_composable0 tm) (Suc s1) (read r) = (Nop, 0::nat)"
      by (rule fetch_mk_composable0_Bk_too_short_Suc)(auto simp add: ‹read r = Bk› ‹length tm ≤ 2 * s1›)
    ultimately have "fetch tm (Suc s1) (read r) = fetch (mk_composable0 tm) (Suc s1) (read r)" by auto
    with ‹(read r) = Bk› and ‹s = Suc s1› have "step0 (s, l, r) tm = step0 (s, l, r) (mk_composable0 tm)" by auto
    with assms have False by auto
    then show ?thesis by auto
  next
    assume "¬ length tm ≤ 2 * s1"    (* a case hard to prove *)
      (* both programs will fetch some action in state s = Suc s1, which is explicitly specified in tm already*)
    then have  "2*s1 < length tm" by auto
    show "step0 (step0 (s, l, r) tm) tm = (0, snd (step0 (s, l, r) tm)) ∧
          step0 (s, l, r) (mk_composable0 tm) = (0, snd (step0 (s, l, r) tm))"
    proof (cases "fetch tm (Suc s1) (read r)")
      fix a1 s'
      assume "fetch tm (Suc s1) (read r) = (a1, s')"
      show ?thesis
      proof (cases "s' ≤ length (mk_composable0 tm) div 2")
        assume "s' ≤ length (mk_composable0 tm) div 2"

        from ‹fetch tm (Suc s1) (read r) = (a1, s')›
          and ‹2*s1 < length tm›
          and ‹(read r) = Bk›
          and ‹s' ≤ length (mk_composable0 tm) div 2›
        have "fetch (mk_composable0 tm) (Suc s1) (read r) = fetch tm (Suc s1) (read r)"
          using fetch_mk_composable0_Bk_Suc_no_fix by auto

        with ‹(read r) = Bk› and ‹s = Suc s1› have "step0 (s, l, r) tm = step0 (s, l, r) (mk_composable0 tm)" by auto
        with assms have False by auto
        then show ?thesis by auto
      next
        assume "¬ s' ≤ length (mk_composable0 tm) div 2"
        then have "length (mk_composable0 tm) div 2 < s'" by auto
        then show ?thesis
        proof (cases s')
          assume "s' = 0"
          with ‹length (mk_composable0 tm) div 2 < s'› have False by auto
          then show ?thesis by auto
        next
          fix s2
          assume "s' = Suc s2"

          from ‹(read r) = Bk› and ‹s = Suc s1› and ‹fetch tm (Suc s1) (read r) = (a1, s')›
          have "step0 (s, l, r) tm = (s', update a1 (l, r))" by auto

          from this and ‹s' = Suc s2› and ‹length (mk_composable0 tm) div 2 < s'›
          have "step0 (step0 (s, l, r) tm) tm = (0, snd (step0 (s, l, r) tm))"
            by (rule jump_out_of_pgm_is_final_next_step)
          moreover have "step0 (s, l, r) (mk_composable0 tm) = (0, snd (step0 (s, l, r) tm))"
          proof -
            from ‹fetch tm (Suc s1) (read r) = (a1, s')›
              and ‹2*s1 < length tm›
              and ‹(read r) = Bk›
              and ‹length (mk_composable0 tm) div 2 < s'›
            have "fetch (mk_composable0 tm) (Suc s1) (read r) = (a1, 0)" using fetch_mk_composable0_Bk_Suc_fix by auto
            with  ‹(read r) = Bk› and ‹s = Suc s1› and ‹fetch tm (Suc s1) (read r) = (a1, s')›
            show ?thesis by auto
          qed
          ultimately  show ?thesis by auto
        qed
      qed
    qed
  qed
next
  fix s1
  assume "read r = Oc" and "s = Suc s1"
  show ?thesis

  proof (cases "length tm ≤ 2*s1+1")  (* both programs will fetch a Nop *)
    assume "length tm ≤ 2 * s1+1"
    with ‹read r = Oc› and ‹s = Suc s1› have "fetch tm (Suc s1) (read r) = (Nop, 0::nat)"
      by (auto)
    moreover have "fetch (mk_composable0 tm) (Suc s1) (read r) = (Nop, 0::nat)"
    proof (rule fetch_mk_composable0_Oc_too_short_Suc)
      from ‹(read r) = Oc› show "(read r) = Oc" .
    next
      from ‹length tm ≤ 2 * s1+1› show "length tm ≤ 2 * s1+1" .
    qed
    ultimately have "fetch tm (Suc s1) (read r) = fetch (mk_composable0 tm) (Suc s1) (read r)" by auto
    with ‹(read r) = Oc› and ‹s = Suc s1› have "step0 (s, l, r) tm = step0 (s, l, r) (mk_composable0 tm)" by auto
    with assms have False by auto
    then show ?thesis by auto
  next
    assume "¬ length tm ≤ 2 * s1+1"  (* a case hard to prove *)
      (* both programs will fetch some action in state s = Suc s1, which is explicitly specified in tm already*)
    then have  "2*s1+1 < length tm" by auto
    show "step0 (step0 (s, l, r) tm) tm = (0, snd (step0 (s, l, r) tm)) ∧
          step0 (s, l, r) (mk_composable0 tm) = (0, snd (step0 (s, l, r) tm))"
    proof (cases "fetch tm (Suc s1) (read r)")
      fix a1 s'
      assume "fetch tm (Suc s1) (read r) = (a1, s')"
      show ?thesis
      proof (cases "s' ≤ length (mk_composable0 tm) div 2")
        assume "s' ≤ length (mk_composable0 tm) div 2"

        from ‹fetch tm (Suc s1) (read r) = (a1, s')›
          and ‹2*s1+1 < length tm›
          and ‹(read r) = Oc›
          and ‹s' ≤ length (mk_composable0 tm) div 2›
        have "fetch (mk_composable0 tm) (Suc s1) (read r) = fetch tm (Suc s1) (read r)"
          using fetch_mk_composable0_Oc_Suc_no_fix by auto

        with ‹(read r) = Oc› and ‹s = Suc s1› have "step0 (s, l, r) tm = step0 (s, l, r) (mk_composable0 tm)" by auto
        with assms have False by auto
        then show ?thesis by auto

      next
        assume "¬ s' ≤ length (mk_composable0 tm) div 2"
        then have "length (mk_composable0 tm) div 2 < s'" by auto
        then show ?thesis
        proof (cases s')
          assume "s' = 0"
          with ‹length (mk_composable0 tm) div 2 < s'› have False by auto
          then show ?thesis by auto
        next
          fix s2
          assume "s' = Suc s2"

          from ‹(read r) = Oc› and ‹s = Suc s1› and ‹fetch tm (Suc s1) (read r) = (a1, s')›
          have "step0 (s, l, r) tm = (s', update a1 (l, r))" by auto

          from this and ‹s' = Suc s2› and ‹length (mk_composable0 tm) div 2 < s'›
          have "step0 (step0 (s, l, r) tm) tm = (0, snd (step0 (s, l, r) tm))"
            by (rule jump_out_of_pgm_is_final_next_step)
          moreover have "step0 (s, l, r) (mk_composable0 tm) = (0, snd (step0 (s, l, r) tm))"
          proof -
            from ‹fetch tm (Suc s1) (read r) = (a1, s')›
              and ‹2*s1+1 < length tm›
              and ‹(read r) = Oc›
              and ‹length (mk_composable0 tm) div 2 < s'›
            have "fetch (mk_composable0 tm) (Suc s1) (read r) = (a1, 0)" using fetch_mk_composable0_Oc_Suc_fix by auto
            with  ‹(read r) = Oc› and ‹s = Suc s1› and ‹fetch tm (Suc s1) (read r) = (a1, s')›
            show ?thesis by auto
          qed
          ultimately  show ?thesis by auto
        qed
      qed
    qed
  qed
qed

lemma step0_mk_composable0_eq_after_two_steps:
  assumes "step0 (s, (l, r)) tm ≠ step0 (s, l, r) (mk_composable0 tm)"
  shows "step0 (step0 (s, (l, r)) tm) tm = (0, snd((step0 (s, (l, r)) tm))) ∧
         step0 (step0 (s, (l, r)) (mk_composable0 tm)) (mk_composable0 tm) = step0 (step0 (s, (l, r)) tm) tm"
proof -
  from assms have A: "step0 (step0 (s, (l, r)) tm) tm = (0, snd((step0 (s, (l, r)) tm))) ∧
         step0 (s, l, r) (mk_composable0 tm)     = (0, snd((step0 (s, (l, r)) tm)))"
    by (rule step0_mk_composable0_after_one_step)
  from A have A1: "step0 (step0 (s, (l, r)) tm) tm = (0, snd((step0 (s, (l, r)) tm)))" by auto
  from A have A2: "step0 (s, l, r) (mk_composable0 tm) = (0, snd((step0 (s, (l, r)) tm)))" by auto

  show ?thesis
  proof (cases "snd((step0 (s, (l, r)) tm))")
    case (Pair a b)
    assume "snd (step0 (s, l, r) tm) = (a, b)"
    show ?thesis
    proof -
      from ‹snd (step0 (s, l, r) tm) = (a, b)› and ‹step0 (s, l, r) (mk_composable0 tm) = (0, snd((step0 (s, (l, r)) tm)))›
      have "step0 (s, l, r) (mk_composable0 tm) = (0, (a,b))" by auto

      then have "step0 (step0 (s, (l, r)) (mk_composable0 tm)) (mk_composable0 tm) = step0 (0, (a,b))  (mk_composable0 tm)" by auto
      also have "... = (0, (a,b))" by auto
      finally have "step0 (step0 (s, (l, r)) (mk_composable0 tm)) (mk_composable0 tm) = (0, (a,b))" by auto

      moreover from A1 and  ‹snd (step0 (s, l, r) tm) = (a, b)›
      have "step0 (step0 (s, (l, r)) tm) tm = (0, (a,b))" by auto

      ultimately have "step0 (step0 (s, (l, r)) (mk_composable0 tm)) (mk_composable0 tm) = step0 (step0 (s, (l, r)) tm) tm" by auto
      with A1 show ?thesis by auto
    qed
  qed
qed

(* ------------------------------------------------------------------ *)

subsection ‹Properties of function steps0 with respect to function mk\_composable0›

lemma "steps0 (s, (l, r)) tm 0 = steps0 (s, l, r) (mk_composable0 tm) 0"
  by auto

lemma mk_composable0_tm_at_most_one_diff_pre:
  assumes "steps0 (s, (l, r)) tm stp ≠ steps0 (s, l, r) (mk_composable0 tm) stp"
  shows "0<stp ∧ (∃k. k<stp 
            ∧ (∀i ≤ k. steps0 (s, l, r) (mk_composable0 tm) i = steps0 (s, l, r) tm i)
            ∧ (∀j > k+1.
                    steps0 (s, l, r) tm (j) = (0, snd(steps0 (s, l, r) tm (k+1))) ∧ 
                    steps0 (s, l, r) (mk_composable0 tm) j = steps0 (s, l, r) tm j))"
proof -
  have "∃k<stp. (∀i≤k. ¬ steps0 (s, l, r) tm i ≠ steps0 (s, l, r) (mk_composable0 tm) i) ∧ steps0 (s, l, r) tm (Suc k) ≠ steps0 (s, l, r) (mk_composable0 tm) (Suc k)"
  proof (rule ex_least_nat_less)
    show "¬ steps0 (s, l, r) tm 0 ≠ steps0 (s, l, r) (mk_composable0 tm) 0" by auto
  next
    from assms show "steps0 (s, l, r) tm stp ≠ steps0 (s, l, r) (mk_composable0 tm) stp" by auto
  qed
  then obtain k where w_k: "k < stp ∧ (∀i≤k. ¬ steps0 (s, l, r) tm i ≠ steps0 (s, l, r) (mk_composable0 tm) i) ∧ steps0 (s, l, r) tm (Suc k) ≠ steps0 (s, l, r) (mk_composable0 tm) (Suc k)" by blast
  from w_k have F1: "k < stp" by auto
  from w_k have F2: "⋀i. i≤k ⟹ ¬ steps0 (s, l, r) tm i ≠ steps0 (s, l, r) (mk_composable0 tm) i" by auto
  from w_k have F3: "steps0 (s, l, r) tm (k + 1) ≠ steps0 (s, l, r) (mk_composable0 tm) (k + 1)" by auto

  from F3 have F3': "(steps0 (s, l, r) tm (Suc k)) ≠ (steps0 (s, l, r) (mk_composable0 tm) (Suc k))" by auto

  have "¬(steps0 (s, l, r) tm k ≠ steps0 (s, l, r) (mk_composable0 tm) k)" using F2 by auto
  then have F4: "steps0 (s, l, r) tm k = steps0 (s, l, r) (mk_composable0 tm) k" by auto

  have X1: "steps0 (s, l, r) (mk_composable0 tm) (Suc k) = step0 (steps0 (s, l, r) (mk_composable0 tm) k) (mk_composable0 tm)" by (rule step_red)
  have X2: "steps0 (s, l, r) tm (Suc k) = step0 (steps0 (s, l, r) tm k) tm" by (rule step_red)

  from X1 and X2 and F3'
  have "step0 (steps0 (s, l, r) tm k) tm ≠ step0 (steps0 (s, l, r) (mk_composable0 tm) k) (mk_composable0 tm)" by auto

  then have "∃ sk lk rk. steps0 (s, l, r) tm k = (sk, lk, rk) ∧
                         steps0 (s, l, r) (mk_composable0 tm) k = (sk, lk, rk) ∧
                         step0 (sk, (lk, rk)) tm ≠ step0 (sk, lk, rk) (mk_composable0 tm)"
  proof (cases "steps0 (s, l, r) tm k")
    case (fields s' l' r')
    then have "steps0 (s, l, r) tm k = (s', l', r')" .
    moreover with ‹step0 (steps0 (s, l, r) tm k) tm ≠ step0 (steps0 (s, l, r) (mk_composable0 tm) k) (mk_composable0 tm)› and F4
    have "step0 (s', (l', r')) tm ≠ step0 (s', l', r') (mk_composable0 tm)" by auto

    moreover from ‹steps0 (s, l, r) tm k = (s', l', r')› and F4
    have "steps0 (s, l, r) (mk_composable0 tm) k = (s', l', r')" by auto
    ultimately have "steps0 (s, l, r) tm k = (s', l', r') ∧ steps0 (s, l, r) (mk_composable0 tm) k = (s', l', r') ∧
                     step0 (s', (l', r')) tm ≠ step0 (s', l', r') (mk_composable0 tm)" by auto

    then show ?thesis by blast
  qed

  then obtain sk lk rk where
    w_sk_lk_rk: "steps0 (s, l, r) tm k = (sk, lk, rk) ∧
                 steps0 (s, l, r) (mk_composable0 tm) k = (sk, lk, rk) ∧
                 step0 (sk, (lk, rk)) tm ≠ step0 (sk, lk, rk) (mk_composable0 tm)" by blast

  have Y1: "step0 (step0 (sk, (lk, rk)) tm) tm = (0, snd((step0 (sk, (lk, rk)) tm))) ∧
         step0 (step0 (sk, (lk, rk)) (mk_composable0 tm)) (mk_composable0 tm) = step0 (step0 (sk, (lk, rk)) tm) tm"
  proof (rule  step0_mk_composable0_eq_after_two_steps)
    from w_sk_lk_rk show "step0 (sk, lk, rk) tm ≠ step0 (sk, lk, rk) (mk_composable0 tm)" by auto
  qed

  from Y1 and w_sk_lk_rk
  have "step0 (step0 (steps0 (s, l, r) tm k) tm) tm = (0, snd((step0 (steps0 (s, l, r) tm k) tm)))" by auto

  from Y1 and w_sk_lk_rk
  have "step0 (step0 (steps0 (s, l, r) (mk_composable0 tm) k) (mk_composable0 tm)) (mk_composable0 tm) = step0 (step0 (steps0 (s, l, r) tm k) tm) tm" by auto

  have "steps0 (s, l, r) (mk_composable0 tm) (k+2) = step0 (step0 (steps0 (s, l, r) (mk_composable0 tm) k) (mk_composable0 tm)) (mk_composable0 tm)"
    by (auto simp add: step_red[symmetric])

  have "steps0 (s, l, r) tm (k+2) = step0 (step0 (steps0 (s, l, r) tm k) tm) tm"
    by (auto simp add: step_red[symmetric])

  from ‹step0 (step0 (steps0 (s, l, r) tm k) tm) tm = (0, snd((step0 (steps0 (s, l, r) tm k) tm)))›
    and ‹steps0 (s, l, r) tm (k+2) = step0 (step0 (steps0 (s, l, r) tm k) tm) tm›
  have "steps0 (s, l, r) tm (k+2) = (0, snd((step0 (steps0 (s, l, r) tm k) tm)))" by auto
  then have N1: "steps0 (s, l, r) tm (k+2) = (0, snd(steps0 (s, l, r) tm (k+1)))" by (auto simp add: step_red[symmetric])

  from ‹step0 (step0 (steps0 (s, l, r) (mk_composable0 tm) k) (mk_composable0 tm)) (mk_composable0 tm) = step0 (step0 (steps0 (s, l, r) tm k) tm) tm›
  have N2: "steps0 (s, l, r) (mk_composable0 tm) (k+2) = steps0 (s, l, r) tm (k+2)" by (auto simp add: step_red[symmetric])

  have N4: "∀j > k+1.
         steps0 (s, l, r) tm (j) = (0, snd(steps0 (s, l, r) tm (k+1))) ∧ 
         steps0 (s, l, r) (mk_composable0 tm) j = steps0 (s, l, r) tm j"
  proof
    fix j
    show "k + 1 < j ⟶ steps0 (s, l, r) tm j = (0, snd (steps0 (s, l, r) tm (k+1))) ∧ steps0 (s, l, r) (mk_composable0 tm) j = steps0 (s, l, r) tm j"
    proof (induct j)
      case 0
      then show ?case by auto
    next
      fix  j
      assume IV: "k + 1 < j ⟶ steps0 (s, l, r) tm j = (0, snd (steps0 (s, l, r) tm (k+1))) ∧ steps0 (s, l, r) (mk_composable0 tm) j = steps0 (s, l, r) tm j"
      show "k + 1 < Suc j ⟶ steps0 (s, l, r) tm (Suc j) = (0, snd (steps0 (s, l, r) tm (k+1))) ∧ steps0 (s, l, r) (mk_composable0 tm) (Suc j) = steps0 (s, l, r) tm (Suc j)"
      proof
        assume "k + 1 < Suc j"
        then have "k + 1 ≤ j" by arith
        then have "k + 1 = j ∨ k+1 < j" by arith 
        then show "steps0 (s, l, r) tm (Suc j) = (0, snd (steps0 (s, l, r) tm (k+1))) ∧ steps0 (s, l, r) (mk_composable0 tm) (Suc j) = steps0 (s, l, r) tm (Suc j)"
        proof
          assume "k + 1 = j"
          with N1 and N2 show "steps0 (s, l, r) tm (Suc j) = (0, snd (steps0 (s, l, r) tm (k+1))) ∧
                               steps0 (s, l, r) (mk_composable0 tm) (Suc j) = steps0 (s, l, r) tm (Suc j)"
            by force
        next
          assume "k + 1 < j"
          with IV
          have Y4: "steps0 (s, l, r) tm j = (0, snd (steps0 (s, l, r) tm (k+1))) ∧ steps0 (s, l, r) (mk_composable0 tm) j = steps0 (s, l, r) tm j" by auto
          show "steps0 (s, l, r) tm (Suc j) = (0, snd (steps0 (s, l, r) tm (k+1))) ∧ steps0 (s, l, r) (mk_composable0 tm) (Suc j) = steps0 (s, l, r) tm (Suc j)"
          proof (cases " snd (steps0 (s, l, r) tm (k+1))")
            case (Pair a b)
            then have "snd (steps0 (s, l, r) tm (k + 1)) = (a, b)" .
            with Y4 have "steps0 (s, l, r) tm j = (0,a,b) ∧ steps0 (s, l, r) (mk_composable0 tm) j = (0,a,b)" by auto
            then have "steps0 (s, l, r) tm (j+1) = (0,a,b) ∧ steps0 (s, l, r) (mk_composable0 tm) (j+1) = (0,a,b)"
            proof
              assume "steps0 (s, l, r) tm j = (0, a, b)" and "steps0 (s, l, r) (mk_composable0 tm) j = (0, a, b)"
              show "steps0 (s, l, r) tm (j + 1) = (0, a, b) ∧ steps0 (s, l, r) (mk_composable0 tm) (j + 1) = (0, a, b)"
              proof
                from ‹steps0 (s, l, r) tm j = (0, a, b)› show "steps0 (s, l, r) tm (j + 1) = (0, a, b)" by (rule stable_config_after_final_add_2)
              next
                from ‹steps0 (s, l, r) (mk_composable0 tm) j = (0, a, b)› show "steps0 (s, l, r) (mk_composable0 tm) (j + 1) = (0, a, b)" by (rule stable_config_after_final_add_2)
              qed
            qed       
            then have "steps0 (s, l, r) tm (Suc j) = (0, a, b) ∧ steps0 (s, l, r) (mk_composable0 tm) (Suc j) = (0, a, b)" by auto
            with ‹snd (steps0 (s, l, r) tm (k + 1)) = (a, b)› show ?thesis by auto
          qed
        qed
      qed
    qed
  qed

  from F1 and F2 and N4 show ?thesis
    by (metis neq0_conv not_less_zero)
qed

(* ----------------- *)

lemma mk_composable0_tm_at_most_one_diff:
  assumes "steps0 (s, l, r) (mk_composable0 tm) stp ≠ steps0 (s, (l, r)) tm stp"
  shows "0<stp ∧  
         (∀i < stp. steps0 (s, l, r) (mk_composable0 tm) i = steps0 (s, l, r) tm i) ∧
         (∀j > stp. steps0 (s, l, r) tm (j) = (0, snd(steps0 (s, l, r) tm stp)) ∧ 
                    steps0 (s, l, r) (mk_composable0 tm) j = steps0 (s, l, r) tm j)"
proof -
  from assms have "steps0 (s, (l, r)) tm stp ≠ steps0 (s, l, r) (mk_composable0 tm) stp" by auto
  then have A:
    "0<stp ∧ (∃k. k<stp 
            ∧ (∀i ≤ k. steps0 (s, l, r) (mk_composable0 tm) i = steps0 (s, l, r) tm i)
            ∧ (∀j > k+1.
                    steps0 (s, l, r) tm (j) = (0, snd(steps0 (s, l, r) tm (k+1))) ∧ 
                    steps0 (s, l, r) (mk_composable0 tm) j = steps0 (s, l, r) tm j))"
    by (rule mk_composable0_tm_at_most_one_diff_pre)
  then have F1: "0<stp" by auto
  from A have "(∃k. k<stp 
            ∧ (∀i ≤ k. steps0 (s, l, r) (mk_composable0 tm) i = steps0 (s, l, r) tm i)
            ∧ (∀j > k+1.
                    steps0 (s, l, r) tm (j) = (0, snd(steps0 (s, l, r) tm (k+1))) ∧ 
                    steps0 (s, l, r) (mk_composable0 tm) j = steps0 (s, l, r) tm j))" by auto
  then obtain k where w_k:
    "k<stp 
            ∧ (∀i ≤ k. steps0 (s, l, r) (mk_composable0 tm) i = steps0 (s, l, r) tm i)
            ∧ (∀j > k+1.
                    steps0 (s, l, r) tm (j) = (0, snd(steps0 (s, l, r) tm (k+1))) ∧ 
                    steps0 (s, l, r) (mk_composable0 tm) j = steps0 (s, l, r) tm j)" by blast
  then have "stp = k+1 ∨ k+1 < stp" by arith
  then show ?thesis
  proof
    assume "stp = k+1"
    show ?thesis
    proof
      from F1 show "0 < stp" by auto
    next
      from ‹stp = k+1› and w_k
      show  "(∀i<stp. steps0 (s, l, r) (mk_composable0 tm) i = steps0 (s, l, r) tm i) ∧
    (∀j>stp. steps0 (s, l, r) tm j = (0, snd (steps0 (s, l, r) tm stp)) ∧ steps0 (s, l, r) (mk_composable0 tm) j = steps0 (s, l, r) tm j)" by auto
    qed
  next
    assume "k+1 < stp"
    with w_k and assms have False by auto
    then show ?thesis by auto
  qed
qed


lemma mk_composable0_tm_at_most_one_diff':
  assumes "steps0 (s, l, r) (mk_composable0 tm) stp ≠ steps0 (s, (l, r)) tm stp"
  shows "0 < stp ∧ (∃fl fr. snd(steps0 (s, l, r) tm stp) = (fl, fr) ∧      
                   (∀i < stp. steps0 (s, l, r) (mk_composable0 tm) i = steps0 (s, l, r) tm i) ∧
                   (∀j > stp. steps0 (s, l, r)  tm         j = (0, fl, fr) ∧ 
                              steps0 (s, l, r) (mk_composable0 tm) j = (0, fl, fr) ))"
proof -
  from assms have major: "0 < stp ∧  
         (∀i < stp. steps0 (s, l, r) (mk_composable0 tm) i = steps0 (s, l, r) tm i) ∧
         (∀j > stp. steps0 (s, l, r) tm (j) = (0, snd(steps0 (s, l, r) tm stp)) ∧ 
                    steps0 (s, l, r) (mk_composable0 tm) j = steps0 (s, l, r) tm j)"
    by (rule mk_composable0_tm_at_most_one_diff)
  from major have F1: "0 < stp" by auto
  from major have F2: "(∀i < stp. steps0 (s, l, r) (mk_composable0 tm) i = steps0 (s, l, r) tm i) ∧
                       (∀j > stp. steps0 (s, l, r) tm (j) = (0, snd(steps0 (s, l, r) tm stp)) ∧ 
                                  steps0 (s, l, r) (mk_composable0 tm) j = steps0 (s, l, r) tm j)" by auto
  then have "snd(steps0 (s, l, r) tm stp) = (fst(snd(steps0 (s, l, r) tm stp)), snd(snd(steps0 (s, l, r) tm stp)) )" by auto
  with F2 have "snd(steps0 (s, l, r) tm stp) = (fst(snd(steps0 (s, l, r) tm stp)), snd(snd(steps0 (s, l, r) tm stp)) ) ∧
                       (∀i < stp. steps0 (s, l, r) (mk_composable0 tm) i = steps0 (s, l, r) tm i) ∧
                       (∀j > stp. steps0 (s, l, r) tm j = (0, (fst(snd(steps0 (s, l, r) tm stp)), snd(snd(steps0 (s, l, r) tm stp)) )) ∧
                                  steps0 (s, l, r) (mk_composable0 tm) j = (0, (fst(snd(steps0 (s, l, r) tm stp)), snd(snd(steps0 (s, l, r) tm stp)) )))"
    by auto
  then have  "(∃fl fr.  snd(steps0 (s, l, r) tm stp) = (fl, fr) ∧
                       (∀i < stp. steps0 (s, l, r) (mk_composable0 tm) i = steps0 (s, l, r) tm i) ∧
                       (∀j > stp. steps0 (s, l, r) tm j = (0, fl, fr) ∧
                                  steps0 (s, l, r) (mk_composable0 tm) j = (0, fl, fr)))" by blast
  with F1 show ?thesis by auto
qed

end