Theory Correctness

(*  Title:       Information Flow Control via Stateful Intransitive Noninterference in Language IMP
    Author:      Pasquale Noce
                 Senior Staff Firmware Engineer at HID Global, Italy
                 pasquale dot noce dot lavoro at gmail dot com
                 pasquale dot noce at hidglobal dot com
*)

section "Sufficiency of well-typedness for information flow correctness"

theory Correctness
  imports Overapproximation
begin

text ‹
\null

The purpose of this section is to prove that type system @{const [names_short] noninterf.ctyping2}
is correct in that it guarantees that well-typed programs satisfy the information flow correctness
criterion expressed by predicate @{const [names_short] noninterf.correct}, namely that if the type
system outputs a value other than @{const None} (that is, a \emph{pass} verdict) when it is input
program @{term c}, @{typ "state set"} @{term A}, and @{typ "vname set"} @{term X}, then
@{prop "correct c A X"} (theorem @{text ctyping2_correct}).

This proof makes use of the lemmas @{text ctyping1_idem} and @{text ctyping2_approx} proven in the
previous sections.
›


subsection "Global context proofs"

lemma flow_append_1:
  assumes A: "⋀cfs' :: (com × state) list.
    c # map fst (cfs :: (com × state) list) = map fst cfs' ⟹
      flow_aux (map fst cfs' @ map fst cfs'') =
      flow_aux (map fst cfs') @ flow_aux (map fst cfs'')"
  shows "flow_aux (c # map fst cfs @ map fst cfs'') =
    flow_aux (c # map fst cfs) @ flow_aux (map fst cfs'')"
using A [of "(c, λx. 0) # cfs"] by simp

lemma flow_append:
 "flow (cfs @ cfs') = flow cfs @ flow cfs'"
by (simp add: flow_def, induction "map fst cfs" arbitrary: cfs
 rule: flow_aux.induct, auto, rule flow_append_1)

lemma flow_cons:
 "flow (cf # cfs) = flow_aux (fst cf # []) @ flow cfs"
by (subgoal_tac "cf # cfs = [cf] @ cfs", simp only: flow_append,
 simp_all add: flow_def)

lemma small_stepsl_append:
 "⟦(c, s) →*{cfs} (c', s'); (c', s') →*{cfs'} (c'', s'')⟧ ⟹
    (c, s) →*{cfs @ cfs'} (c'', s'')"
by (induction c' s' cfs' c'' s'' rule: small_stepsl_induct,
 simp, simp only: append_assoc [symmetric] small_stepsl.simps)


lemma small_stepsl_cons_1:
 "(c, s) →*{[cf]} (c'', s'') ⟹
    cf = (c, s) ∧
    (∃c' s'. (c, s) → (c', s') ∧ (c', s') →*{[]} (c'', s''))"
by (subst (asm) append_Nil [symmetric],
 simp only: small_stepsl.simps, simp)

lemma small_stepsl_cons_2:
 "⟦(c, s) →*{cf # cfs} (c'', s'') ⟹
    cf = (c, s) ∧
    (∃c' s'. (c, s) → (c', s') ∧ (c', s') →*{cfs} (c'', s''));
  (c, s) →*{cf # cfs @ [(c'', s'')]} (c''', s''')⟧ ⟹
    cf = (c, s) ∧
    (∃c' s'. (c, s) → (c', s') ∧
      (c', s') →*{cfs @ [(c'', s'')]} (c''', s'''))"
by (simp only: append_Cons [symmetric],
 simp only: small_stepsl.simps, simp)

lemma small_stepsl_cons:
 "(c, s) →*{cf # cfs} (c'', s'') ⟹
    cf = (c, s) ∧
    (∃c' s'. (c, s) → (c', s') ∧ (c', s') →*{cfs} (c'', s''))"
by (induction c s cfs c'' s'' rule: small_stepsl_induct,
 erule small_stepsl_cons_1, rule small_stepsl_cons_2)


lemma small_steps_stepsl_1:
 "∃cfs. (c, s) →*{cfs} (c, s)"
by (rule exI [of _ "[]"], simp)

lemma small_steps_stepsl_2:
 "⟦(c, s) → (c', s'); (c', s') →*{cfs} (c'', s'')⟧ ⟹
    ∃cfs'. (c, s) →*{cfs'} (c'', s'')"
by (rule exI [of _ "[(c, s)] @ cfs"], rule small_stepsl_append
 [where c' = c' and s' = s'], subst append_Nil [symmetric],
 simp only: small_stepsl.simps)

lemma small_steps_stepsl:
 "(c, s) →* (c', s') ⟹ ∃cfs. (c, s) →*{cfs} (c', s')"
by (induction c s c' s' rule: star_induct,
 rule small_steps_stepsl_1, blast intro: small_steps_stepsl_2)

lemma small_stepsl_steps:
 "(c, s) →*{cfs} (c', s') ⟹ (c, s) →* (c', s')"
by (induction c s cfs c' s' rule: small_stepsl_induct,
 auto intro: star_trans)

lemma small_stepsl_skip:
 "(SKIP, s) →*{cfs} (c, t) ⟹
    (c, t) = (SKIP, s) ∧ flow cfs = []"
by (induction SKIP s cfs c t rule: small_stepsl_induct,
 auto simp: flow_def)


lemma small_stepsl_assign_1:
 "(x ::= a, s) →*{[]} (c', s') ⟹
    (c', s') = (x ::= a, s) ∧ flow [] = [] ∨
    (c', s') = (SKIP, s(x := aval a s)) ∧ flow [] = [x ::= a]"
by (simp add: flow_def)

lemma small_stepsl_assign_2:
 "⟦(x ::= a, s) →*{cfs} (c', s') ⟹
    (c', s') = (x ::= a, s) ∧ flow cfs = [] ∨
      (c', s') = (SKIP, s(x := aval a s)) ∧ flow cfs = [x ::= a];
    (x ::= a, s) →*{cfs @ [(c', s')]} (c'', s'')⟧ ⟹
  (c'', s'') = (x ::= a, s) ∧
    flow (cfs @ [(c', s')]) = [] ∨
  (c'', s'') = (SKIP, s(x := aval a s)) ∧
    flow (cfs @ [(c', s')]) = [x ::= a]"
by (auto, (simp add: flow_append, simp add: flow_def)+)

lemma small_stepsl_assign:
 "(x ::= a, s) →*{cfs} (c, t) ⟹
    (c, t) = (x ::= a, s) ∧ flow cfs = [] ∨
    (c, t) = (SKIP, s(x := aval a s)) ∧ flow cfs = [x ::= a]"
by (induction "x ::= a :: com" s cfs c t rule: small_stepsl_induct,
 erule small_stepsl_assign_1, rule small_stepsl_assign_2)


lemma small_stepsl_seq_1:
 "(c⇩1;; c⇩2, s) →*{[]} (c', s') ⟹
    (∃c'' cfs'. c' = c'';; c⇩2 ∧
      (c⇩1, s) →*{cfs'} (c'', s') ∧
      flow [] = flow cfs') ∨
    (∃s'' cfs' cfs''. length cfs'' < length [] ∧
      (c⇩1, s) →*{cfs'} (SKIP, s'') ∧
      (c⇩2, s'') →*{cfs''} (c', s') ∧
      flow [] = flow cfs' @ flow cfs'')"
by force

lemma small_stepsl_seq_2:
  assumes
    A: "(c⇩1;; c⇩2, s) →*{cfs} (c', s') ⟹
      (∃c'' cfs'. c' = c'';; c⇩2 ∧
        (c⇩1, s) →*{cfs'} (c'', s') ∧
        flow cfs = flow cfs') ∨
      (∃s'' cfs' cfs''. length cfs'' < length cfs ∧
        (c⇩1, s) →*{cfs'} (SKIP, s'') ∧
        (c⇩2, s'') →*{cfs''} (c', s') ∧
        flow cfs = flow cfs' @ flow cfs'')" and
    B: "(c⇩1;; c⇩2, s) →*{cfs @ [(c', s')]} (c'', s'')"
  shows
   "(∃d cfs'. c'' = d;; c⇩2 ∧
      (c⇩1, s) →*{cfs'} (d, s'') ∧
      flow (cfs @ [(c', s')]) = flow cfs') ∨
    (∃t cfs' cfs''. length cfs'' < length (cfs @ [(c', s')]) ∧
      (c⇩1, s) →*{cfs'} (SKIP, t) ∧
      (c⇩2, t) →*{cfs''} (c'', s'') ∧
      flow (cfs @ [(c', s')]) = flow cfs' @ flow cfs'')"
    (is "?P ∨ ?Q")
proof -
  {
    assume C: "(c', s') → (c'', s'')"
    assume
     "(∃d. c' = d;; c⇩2 ∧ (∃cfs'.
        (c⇩1, s) →*{cfs'} (d, s') ∧
        flow cfs = flow cfs')) ∨
      (∃t cfs' cfs''. length cfs'' < length cfs ∧
        (c⇩1, s) →*{cfs'} (SKIP, t) ∧
        (c⇩2, t) →*{cfs''} (c', s') ∧
        flow cfs = flow cfs' @ flow cfs'')"
      (is "(∃d. ?R d ∧ (∃cfs'. ?S d cfs')) ∨
        (∃t cfs' cfs''. ?T t cfs' cfs'')")
    hence ?thesis
    proof
      assume "∃c''. ?R c'' ∧ (∃cfs'. ?S c'' cfs')"
      then obtain d and cfs' where
        D: "c' = d;; c⇩2" and
        E: "(c⇩1, s) →*{cfs'} (d, s')" and
        F: "flow cfs = flow cfs'"
        by blast
      hence "(d;; c⇩2, s') → (c'', s'')"
        using C by simp
      moreover {
        assume
          G: "d = SKIP" and
          H: "(c'', s'') = (c⇩2, s')"
        have ?Q
        proof (rule exI [of _ s'], rule exI [of _ cfs'],
         rule exI [of _ "[]"])
          from D and E and F and G and H show
           "length [] < length (cfs @ [(c', s')]) ∧
            (c⇩1, s) →*{cfs'} (SKIP, s') ∧
            (c⇩2, s') →*{[]} (c'', s'') ∧
            flow (cfs @ [(c', s')]) = flow cfs' @ flow []"
            by (simp add: flow_append, simp add: flow_def)
        qed
      }
      moreover {
        fix d' t'
        assume
          G: "(d, s') → (d', t')" and
          H: "(c'', s'') = (d';; c⇩2, t')"
        have ?P
        proof (rule exI [of _ d'], rule exI [of _ "cfs' @ [(d, s')]"])
          from D and E and F and G and H show
           "c'' = d';; c⇩2 ∧
            (c⇩1, s) →*{cfs' @ [(d, s')]} (d', s'') ∧
            flow (cfs @ [(c', s')]) = flow (cfs' @ [(d, s')])"
            by (simp add: flow_append, simp add: flow_def)
        qed
      }
      ultimately show ?thesis
        by blast
    next
      assume "∃t cfs' cfs''. ?T t cfs' cfs''"
      then obtain t and cfs' and cfs'' where
        D: "length cfs'' < length cfs" and
        E: "(c⇩1, s) →*{cfs'} (SKIP, t)" and
        F: "(c⇩2, t) →*{cfs''} (c', s')" and
        G: "flow cfs = flow cfs' @ flow cfs''"
        by blast
      show ?thesis
      proof (rule disjI2, rule exI [of _ t], rule exI [of _ cfs'],
       rule exI [of _ "cfs'' @ [(c', s')]"])
        from C and D and E and F and G show
         "length (cfs'' @ [(c', s')]) < length (cfs @ [(c', s')]) ∧
          (c⇩1, s) →*{cfs'} (SKIP, t) ∧
          (c⇩2, t) →*{cfs'' @ [(c', s')]} (c'', s'') ∧
          flow (cfs @ [(c', s')]) =
            flow cfs' @ flow (cfs'' @ [(c', s')])"
          by (simp add: flow_append)
      qed
    qed
  }
  with A and B show ?thesis
    by simp
qed

lemma small_stepsl_seq:
 "(c⇩1;; c⇩2, s) →*{cfs} (c, t) ⟹
    (∃c' cfs'. c = c';; c⇩2 ∧
      (c⇩1, s) →*{cfs'} (c', t) ∧
      flow cfs = flow cfs') ∨
    (∃s' cfs' cfs''. length cfs'' < length cfs ∧
      (c⇩1, s) →*{cfs'} (SKIP, s') ∧ (c⇩2, s') →*{cfs''} (c, t) ∧
      flow cfs = flow cfs' @ flow cfs'')"
by (induction "c⇩1;; c⇩2" s cfs c t arbitrary: c⇩1 c⇩2
 rule: small_stepsl_induct, erule small_stepsl_seq_1,
 rule small_stepsl_seq_2)


lemma small_stepsl_if_1:
 "(IF b THEN c⇩1 ELSE c⇩2, s) →*{[]} (c', s') ⟹
    (c', s') = (IF b THEN c⇩1 ELSE c⇩2, s) ∧
      flow [] = [] ∨
    bval b s ∧ (c⇩1, s) →*{tl []} (c', s') ∧
      flow [] = ⟨bvars b⟩ # flow (tl []) ∨
    ¬ bval b s ∧ (c⇩2, s) →*{tl []} (c', s') ∧
      flow [] = ⟨bvars b⟩ # flow (tl [])"
by (simp add: flow_def)

lemma small_stepsl_if_2:
  assumes
    A: "(IF b THEN c⇩1 ELSE c⇩2, s) →*{cfs} (c', s') ⟹
      (c', s') = (IF b THEN c⇩1 ELSE c⇩2, s) ∧
        flow cfs = [] ∨
      bval b s ∧ (c⇩1, s) →*{tl cfs} (c', s') ∧
        flow cfs = ⟨bvars b⟩ # flow (tl cfs) ∨
      ¬ bval b s ∧ (c⇩2, s) →*{tl cfs} (c', s') ∧
        flow cfs = ⟨bvars b⟩ # flow (tl cfs)" and
    B: "(IF b THEN c⇩1 ELSE c⇩2, s) →*{cfs @ [(c', s')]} (c'', s'')"
  shows
   "(c'', s'') = (IF b THEN c⇩1 ELSE c⇩2, s) ∧
      flow (cfs @ [(c', s')]) = [] ∨
    bval b s ∧ (c⇩1, s) →*{tl (cfs @ [(c', s')])} (c'', s'') ∧
      flow (cfs @ [(c', s')]) = ⟨bvars b⟩ # flow (tl (cfs @ [(c', s')])) ∨
    ¬ bval b s ∧ (c⇩2, s) →*{tl (cfs @ [(c', s')])} (c'', s'') ∧
      flow (cfs @ [(c', s')]) = ⟨bvars b⟩ # flow (tl (cfs @ [(c', s')]))"
    (is "_ ∨ ?P")
proof -
  {
    assume
      C: "(IF b THEN c⇩1 ELSE c⇩2, s) →*{cfs} (c', s')" and
      D: "(c', s') → (c'', s'')"
    assume
     "c' = IF b THEN c⇩1 ELSE c⇩2 ∧ s' = s ∧
        flow cfs = [] ∨
      bval b s ∧ (c⇩1, s) →*{tl cfs} (c', s') ∧
        flow cfs = ⟨bvars b⟩ # flow (tl cfs) ∨
      ¬ bval b s ∧ (c⇩2, s) →*{tl cfs} (c', s') ∧
        flow cfs = ⟨bvars b⟩ # flow (tl cfs)"
      (is "?Q ∨ ?R ∨ ?S")
    hence ?P
    proof (rule disjE, erule_tac [2] disjE)
      assume ?Q
      moreover from this have "(IF b THEN c⇩1 ELSE c⇩2, s) → (c'', s'')"
        using D by simp
      ultimately show ?thesis
        using C by (erule_tac IfE, auto dest: small_stepsl_cons
         simp: tl_append flow_cons split: list.split)
    next
      assume ?R
      with C and D show ?thesis
        by (auto simp: tl_append flow_cons split: list.split)
    next
      assume ?S
      with C and D show ?thesis
        by (auto simp: tl_append flow_cons split: list.split)
    qed
  }
  with A and B show ?thesis
    by simp
qed

lemma small_stepsl_if:
 "(IF b THEN c⇩1 ELSE c⇩2, s) →*{cfs} (c, t) ⟹
    (c, t) = (IF b THEN c⇩1 ELSE c⇩2, s) ∧
      flow cfs = [] ∨
    bval b s ∧ (c⇩1, s) →*{tl cfs} (c, t) ∧
      flow cfs = ⟨bvars b⟩ # flow (tl cfs) ∨
    ¬ bval b s ∧ (c⇩2, s) →*{tl cfs} (c, t) ∧
      flow cfs = ⟨bvars b⟩ # flow (tl cfs)"
by (induction "IF b THEN c⇩1 ELSE c⇩2" s cfs c t arbitrary: b c⇩1 c⇩2
 rule: small_stepsl_induct, erule small_stepsl_if_1,
 rule small_stepsl_if_2)


lemma small_stepsl_while_1:
 "(WHILE b DO c, s) →*{[]} (c', s') ⟹
    (c', s') = (WHILE b DO c, s) ∧ flow [] = [] ∨
    (IF b THEN c;; WHILE b DO c ELSE SKIP, s) →*{tl []} (c', s') ∧
      flow [] = flow (tl [])"
by (simp add: flow_def)

lemma small_stepsl_while_2:
  assumes
    A: "(WHILE b DO c, s) →*{cfs} (c', s') ⟹
      (c', s') = (WHILE b DO c, s) ∧
        flow cfs = [] ∨
      (IF b THEN c;; WHILE b DO c ELSE SKIP, s) →*{tl cfs} (c', s') ∧
        flow cfs = flow (tl cfs)" and
    B: "(WHILE b DO c, s) →*{cfs @ [(c', s')]} (c'', s'')"
  shows
   "(c'', s'') = (WHILE b DO c, s) ∧
      flow (cfs @ [(c', s')]) = [] ∨
    (IF b THEN c;; WHILE b DO c ELSE SKIP, s)
      →*{tl (cfs @ [(c', s')])} (c'', s'') ∧
      flow (cfs @ [(c', s')]) = flow (tl (cfs @ [(c', s')]))"
    (is "_ ∨ ?P")
proof -
  {
    assume
      C: "(WHILE b DO c, s) →*{cfs} (c', s')" and
      D: "(c', s') → (c'', s'')"
    assume
     "c' = WHILE b DO c ∧ s' = s ∧
        flow cfs = [] ∨
      (IF b THEN c;; WHILE b DO c ELSE SKIP, s) →*{tl cfs} (c', s') ∧
        flow cfs = flow (tl cfs)"
      (is "?Q ∨ ?R")
    hence ?P
    proof
      assume ?Q
      moreover from this have "(WHILE b DO c, s) → (c'', s'')"
        using D by simp
      ultimately show ?thesis
        using C by (erule_tac WhileE, auto dest: small_stepsl_cons
         simp: tl_append flow_cons split: list.split)
    next
      assume ?R
      with C and D show ?thesis
        by (auto simp: tl_append flow_cons split: list.split)
    qed
  }
  with A and B show ?thesis
    by simp
qed

lemma small_stepsl_while:
 "(WHILE b DO c, s) →*{cfs} (c', s') ⟹
    (c', s') = (WHILE b DO c, s) ∧
      flow cfs = [] ∨
    (IF b THEN c;; WHILE b DO c ELSE SKIP, s) →*{tl cfs} (c', s') ∧
      flow cfs = flow (tl cfs)"
by (induction "WHILE b DO c" s cfs c' s' arbitrary: b c
 rule: small_stepsl_induct, erule small_stepsl_while_1,
 rule small_stepsl_while_2)


lemma bvars_bval:
 "s = t (⊆ bvars b) ⟹ bval b s = bval b t"
by (induction b, simp_all, rule arg_cong2, auto intro: avars_aval)

lemma run_flow_append:
 "run_flow (cs @ cs') s = run_flow cs' (run_flow cs s)"
by (induction cs s rule: run_flow.induct, simp_all (no_asm))

lemma no_upd_append:
 "no_upd (cs @ cs') x = (no_upd cs x ∧ no_upd cs' x)"
by (induction cs, simp_all)

lemma no_upd_run_flow:
 "no_upd cs x ⟹ run_flow cs s x = s x"
by (induction cs s rule: run_flow.induct, auto)

lemma small_stepsl_run_flow_1:
 "(c, s) →*{[]} (c', s') ⟹ s' = run_flow (flow []) s"
by (simp add: flow_def)

lemma small_stepsl_run_flow_2:
 "(c, s) → (c', s') ⟹ s' = run_flow (flow_aux [c]) s"
by (induction "[c]" arbitrary: c c' rule: flow_aux.induct, auto)

lemma small_stepsl_run_flow_3:
 "⟦(c, s) →*{cfs} (c', s') ⟹ s' = run_flow (flow cfs) s;
    (c, s) →*{cfs @ [(c', s')]} (c'', s'')⟧ ⟹
  s'' = run_flow (flow (cfs @ [(c', s')])) s"
by (simp add: flow_append run_flow_append,
 auto intro: small_stepsl_run_flow_2 simp: flow_def)

lemma small_stepsl_run_flow:
 "(c, s) →*{cfs} (c', s') ⟹ s' = run_flow (flow cfs) s"
by (induction c s cfs c' s' rule: small_stepsl_induct,
 erule small_stepsl_run_flow_1, rule small_stepsl_run_flow_3)


subsection "Local context proofs"

context noninterf
begin


lemma no_upd_sources:
 "no_upd cs x ⟹ x ∈ sources cs s x"
by (induction cs rule: rev_induct, auto simp: no_upd_append
 split: com_flow.split)

lemma sources_aux_sources:
 "sources_aux cs s x ⊆ sources cs s x"
by (induction cs rule: rev_induct, auto split: com_flow.split)

lemma sources_aux_append:
 "sources_aux cs s x ⊆ sources_aux (cs @ cs') s x"
by (induction cs' rule: rev_induct, simp, subst append_assoc [symmetric],
 auto simp del: append_assoc split: com_flow.split)

lemma sources_aux_observe_hd_1:
 "∀y ∈ X. s: dom y ↝ dom x ⟹ X ⊆ sources_aux [⟨X⟩] s x"
by (subst append_Nil [symmetric], subst sources_aux.simps, auto)

lemma sources_aux_observe_hd_2:
 "(∀y ∈ X. s: dom y ↝ dom x ⟹ X ⊆ sources_aux (⟨X⟩ # xs) s x) ⟹
    ∀y ∈ X. s: dom y ↝ dom x ⟹ X ⊆ sources_aux (⟨X⟩ # xs @ [x']) s x"
by (subst append_Cons [symmetric], subst sources_aux.simps,
 auto split: com_flow.split)

lemma sources_aux_observe_hd:
 "∀y ∈ X. s: dom y ↝ dom x ⟹ X ⊆ sources_aux (⟨X⟩ # cs) s x"
by (induction cs rule: rev_induct,
 erule sources_aux_observe_hd_1, rule sources_aux_observe_hd_2)


lemma sources_observe_tl_1:
  assumes
    A: "⋀z a. c = (x ::= a :: com_flow) ⟹ z = x ⟹
      sources_aux cs s x ⊆ sources_aux (⟨X⟩ # cs) s x" and
    B: "⋀z a y. c = (x ::= a :: com_flow) ⟹ z = x ⟹
      sources cs s y ⊆ sources (⟨X⟩ # cs) s y" and
    C: "⋀z a. c = (z ::= a :: com_flow) ⟹ z ≠ x ⟹
      sources cs s x ⊆ sources (⟨X⟩ # cs) s x" and
    D: "⋀Y y. c = ⟨Y⟩ ⟹
      sources cs s y ⊆ sources (⟨X⟩ # cs) s y" and
    E: "z ∈ (case c of
      z ::= a ⇒ if z = x
        then sources_aux cs s x ∪ ⋃ {sources cs s y | y.
          run_flow cs s: dom y ↝ dom x ∧ y ∈ avars a}
        else sources cs s x |
      ⟨X⟩ ⇒
        sources cs s x ∪ ⋃ {sources cs s y | y.
          run_flow cs s: dom y ↝ dom x ∧ y ∈ X})"
  shows "z ∈ sources (⟨X⟩ # cs @ [c]) s x"
proof -
  {
    fix a
    assume
      F: "∀A. (∀y. run_flow cs s: dom y ↝ dom x ⟶
        A = sources (⟨X⟩ # cs) s y ⟶ y ∉ avars a) ∨ z ∉ A" and
      G: "c = x ::= a"
    have "z ∈ sources_aux cs s x ∪ ⋃ {sources cs s y | y.
      run_flow cs s: dom y ↝ dom x ∧ y ∈ avars a}"
      using E and G by simp
    hence "z ∈ sources_aux (⟨X⟩ # cs) s x"
    using A and G proof (erule_tac UnE, blast)
      assume "z ∈ ⋃ {sources cs s y | y.
        run_flow cs s: dom y ↝ dom x ∧ y ∈ avars a}"
      then obtain y where
        H: "z ∈ sources cs s y" and
        I: "run_flow cs s: dom y ↝ dom x" and
        J: "y ∈ avars a"
        by blast
      have "z ∈ sources (⟨X⟩ # cs) s y"
        using B and G and H by blast
      hence "y ∉ avars a"
        using F and I by blast
      thus ?thesis
        using J by contradiction
    qed
  }
  moreover {
    fix y a
    assume "c = y ::= a" and "y ≠ x"
    moreover from this have "z ∈ sources cs s x"
      using E by simp
    ultimately have "z ∈ sources (⟨X⟩ # cs) s x"
      using C by blast
  }
  moreover {
    fix Y
    assume
      F: "∀A. (∀y. run_flow cs s: dom y ↝ dom x ⟶
        A = sources (⟨X⟩ # cs) s y ⟶ y ∉ Y) ∨ z ∉ A" and
      G: "c = ⟨Y⟩"
    have "z ∈ sources cs s x ∪ ⋃ {sources cs s y | y.
      run_flow cs s: dom y ↝ dom x ∧ y ∈ Y}"
      using E and G by simp
    hence "z ∈ sources (⟨X⟩ # cs) s x"
    using D and G proof (erule_tac UnE, blast)
      assume "z ∈ ⋃ {sources cs s y | y.
        run_flow cs s: dom y ↝ dom x ∧ y ∈ Y}"
      then obtain y where
        H: "z ∈ sources cs s y" and
        I: "run_flow cs s: dom y ↝ dom x" and
        J: "y ∈ Y"
        by blast
      have "z ∈ sources (⟨X⟩ # cs) s y"
        using D and G and H by blast
      hence "y ∉ Y"
        using F and I by blast
      thus ?thesis
        using J by contradiction
    qed
  }
  ultimately show ?thesis
    by (simp only: append_Cons [symmetric] sources.simps,
     auto split: com_flow.split)
qed

lemma sources_observe_tl_2:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹
      sources_aux cs s x ⊆ sources_aux (⟨X⟩ # cs) s x" and
    B: "⋀Y. c = ⟨Y⟩ ⟹
      sources_aux cs s x ⊆ sources_aux (⟨X⟩ # cs) s x" and
    C: "⋀Y y. c = ⟨Y⟩ ⟹
      sources cs s y ⊆ sources (⟨X⟩ # cs) s y" and
    D: "z ∈ (case c of
      z ::= a ⇒
        sources_aux cs s x |
      ⟨X⟩ ⇒
        sources_aux cs s x ∪ ⋃ {sources cs s y | y.
          run_flow cs s: dom y ↝ dom x ∧ y ∈ X})"
  shows "z ∈ sources_aux (⟨X⟩ # cs @ [c]) s x"
proof -
  {
    fix y a
    assume "c = y ::= a"
    moreover from this have "z ∈ sources_aux cs s x"
      using D by simp
    ultimately have "z ∈ sources_aux (⟨X⟩ # cs) s x"
      using A by blast
  }
  moreover {
    fix Y
    assume
      E: "∀A. (∀y. run_flow cs s: dom y ↝ dom x ⟶
        A = sources (⟨X⟩ # cs) s y ⟶ y ∉ Y) ∨ z ∉ A" and
      F: "c = ⟨Y⟩"
    have "z ∈ sources_aux cs s x ∪ ⋃ {sources cs s y | y.
      run_flow cs s: dom y ↝ dom x ∧ y ∈ Y}"
      using D and F by simp
    hence "z ∈ sources_aux (⟨X⟩ # cs) s x"
    using B and F proof (erule_tac UnE, blast)
      assume "z ∈ ⋃ {sources cs s y | y.
        run_flow cs s: dom y ↝ dom x ∧ y ∈ Y}"
      then obtain y where
        H: "z ∈ sources cs s y" and
        I: "run_flow cs s: dom y ↝ dom x" and
        J: "y ∈ Y"
        by blast
      have "z ∈ sources (⟨X⟩ # cs) s y"
        using C and F and H by blast
      hence "y ∉ Y"
        using E and I by blast
      thus ?thesis
        using J by contradiction
    qed
  }
  ultimately show ?thesis
    by (simp only: append_Cons [symmetric] sources_aux.simps,
     auto split: com_flow.split)
qed

lemma sources_observe_tl:
 "sources cs s x ⊆ sources (⟨X⟩ # cs) s x"
and sources_aux_observe_tl:
 "sources_aux cs s x ⊆ sources_aux (⟨X⟩ # cs) s x"
proof (induction cs s x and cs s x rule: sources_induct)
  fix cs c s x
  show
   "⟦⋀z a. c = z ::= a ⟹ z = x ⟹
      sources_aux cs s x ⊆ sources_aux (⟨X⟩ # cs) s x;
    ⋀z a b y. c = z ::= a ⟹ z = x ⟹
      sources cs s y ⊆ sources (⟨X⟩ # cs) s y;
    ⋀z a. c = z ::= a ⟹ z ≠ x ⟹
      sources cs s x ⊆ sources (⟨X⟩ # cs) s x;
    ⋀Y. c = ⟨Y⟩ ⟹
      sources cs s x ⊆ sources (⟨X⟩ # cs) s x;
    ⋀Y a y. c = ⟨Y⟩ ⟹
      sources cs s y ⊆ sources (⟨X⟩ # cs) s y⟧ ⟹
      sources (cs @ [c]) s x ⊆ sources (⟨X⟩ # cs @ [c]) s x"
    by (auto, rule sources_observe_tl_1)
next
  fix s x
  show "sources [] s x ⊆ sources [⟨X⟩] s x"
    by (subst (3) append_Nil [symmetric],
     simp only: sources.simps, simp)
next
  fix cs c s x
  show
   "⟦⋀z a. c = z ::= a ⟹
      sources_aux cs s x ⊆ sources_aux (⟨X⟩ # cs) s x;
    ⋀Y. c = ⟨Y⟩ ⟹
      sources_aux cs s x ⊆ sources_aux (⟨X⟩ # cs) s x;
    ⋀Y a y. c = ⟨Y⟩ ⟹
      sources cs s y ⊆ sources (⟨X⟩ # cs) s y⟧ ⟹
      sources_aux (cs @ [c]) s x ⊆ sources_aux (⟨X⟩ # cs @ [c]) s x"
    by (auto, rule sources_observe_tl_2)
qed simp


lemma sources_member_1:
  assumes
    A: "⋀z a. c = (x ::= a :: com_flow) ⟹ z = x ⟹
      y ∈ sources_aux cs' (run_flow cs s) x ⟹
        sources cs s y ⊆ sources_aux (cs @ cs') s x" and
    B: "⋀z a w. c = (x ::= a :: com_flow) ⟹ z = x ⟹
      y ∈ sources cs' (run_flow cs s) w ⟹
        sources cs s y ⊆ sources (cs @ cs') s w" and
    C: "⋀z a. c = (z ::= a :: com_flow) ⟹ z ≠ x ⟹
      y ∈ sources cs' (run_flow cs s) x ⟹
        sources cs s y ⊆ sources (cs @ cs') s x" and
    D: "⋀Y w. c = ⟨Y⟩ ⟹
      y ∈ sources cs' (run_flow cs s) w ⟹
        sources cs s y ⊆ sources (cs @ cs') s w" and
    E: "y ∈ (case c of
      z ::= a ⇒ if z = x
        then sources_aux cs' (run_flow cs s) x ∪
          ⋃ {sources cs' (run_flow cs s) y | y.
            run_flow cs' (run_flow cs s): dom y ↝ dom x ∧ y ∈ avars a}
        else sources cs' (run_flow cs s) x |
      ⟨X⟩ ⇒
        sources cs' (run_flow cs s) x ∪
          ⋃ {sources cs' (run_flow cs s) y | y.
            run_flow cs' (run_flow cs s): dom y ↝ dom x ∧ y ∈ X})" and
    F: "z ∈ sources cs s y"
  shows "z ∈ sources (cs @ cs' @ [c]) s x"
proof -
  {
    fix a
    assume
      G: "∀A. (∀y. run_flow cs' (run_flow cs s): dom y ↝ dom x ⟶
        A = sources (cs @ cs') s y ⟶ y ∉ avars a) ∨ z ∉ A" and
      H: "c = x ::= a"
    have "y ∈ sources_aux cs' (run_flow cs s) x ∪
      ⋃ {sources cs' (run_flow cs s) y | y.
        run_flow cs' (run_flow cs s): dom y ↝ dom x ∧ y ∈ avars a}"
      using E and H by simp
    hence "z ∈ sources_aux (cs @ cs') s x"
    using A and F and H proof (erule_tac UnE, blast)
      assume "y ∈ ⋃ {sources cs' (run_flow cs s) y | y.
        run_flow cs' (run_flow cs s): dom y ↝ dom x ∧ y ∈ avars a}"
      then obtain w where
        I: "y ∈ sources cs' (run_flow cs s) w" and
        J: "run_flow cs' (run_flow cs s): dom w ↝ dom x" and
        K: "w ∈ avars a"
        by blast
      have "z ∈ sources (cs @ cs') s w"
        using B and F and H and I by blast
      hence "w ∉ avars a"
        using G and J by blast
      thus ?thesis
        using K by contradiction
    qed
  }
  moreover {
    fix w a
    assume "c = w ::= a" and "w ≠ x"
    moreover from this have "y ∈ sources cs' (run_flow cs s) x"
      using E by simp
    ultimately have "z ∈ sources (cs @ cs') s x"
      using C and F by blast
  }
  moreover {
    fix Y
    assume
      G: "∀A. (∀y. run_flow cs' (run_flow cs s): dom y ↝ dom x ⟶
        A = sources (cs @ cs') s y ⟶ y ∉ Y) ∨ z ∉ A" and
      H: "c = ⟨Y⟩"
    have "y ∈ sources cs' (run_flow cs s) x ∪
      ⋃ {sources cs' (run_flow cs s) y | y.
        run_flow cs' (run_flow cs s): dom y ↝ dom x ∧ y ∈ Y}"
      using E and H by simp
    hence "z ∈ sources (cs @ cs') s x"
    using D and F and H proof (erule_tac UnE, blast)
      assume "y ∈ ⋃ {sources cs' (run_flow cs s) y | y.
        run_flow cs' (run_flow cs s): dom y ↝ dom x ∧ y ∈ Y}"
      then obtain w where
        I: "y ∈ sources cs' (run_flow cs s) w" and
        J: "run_flow cs' (run_flow cs s): dom w ↝ dom x" and
        K: "w ∈ Y"
        by blast
      have "z ∈ sources (cs @ cs') s w"
        using D and F and H and I by blast
      hence "w ∉ Y"
        using G and J by blast
      thus ?thesis
        using K by contradiction
    qed
  }
  ultimately show ?thesis
    by (simp only: append_assoc [symmetric] sources.simps,
     auto simp: run_flow_append split: com_flow.split)
qed

lemma sources_member_2:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹
      y ∈ sources_aux cs' (run_flow cs s) x ⟹
        sources cs s y ⊆ sources_aux (cs @ cs') s x" and
    B: "⋀Y. c = ⟨Y⟩ ⟹
      y ∈ sources_aux cs' (run_flow cs s) x ⟹
        sources cs s y ⊆ sources_aux (cs @ cs') s x" and
    C: "⋀Y w. c = ⟨Y⟩ ⟹
      y ∈ sources cs' (run_flow cs s) w ⟹
        sources cs s y ⊆ sources (cs @ cs') s w" and
    D: "y ∈ (case c of
      z ::= a ⇒
        sources_aux cs' (run_flow cs s) x |
      ⟨X⟩ ⇒
        sources_aux cs' (run_flow cs s) x ∪
          ⋃ {sources cs' (run_flow cs s) y | y.
            run_flow cs' (run_flow cs s): dom y ↝ dom x ∧ y ∈ X})" and
    E: "z ∈ sources cs s y"
  shows "z ∈ sources_aux (cs @ cs' @ [c]) s x"
proof -
  {
    fix w a
    assume "c = w ::= a"
    moreover from this have "y ∈ sources_aux cs' (run_flow cs s) x"
      using D by simp
    ultimately have "z ∈ sources_aux (cs @ cs') s x"
      using A and E by blast
  }
  moreover {
    fix Y
    assume
      G: "∀A. (∀y. run_flow cs' (run_flow cs s): dom y ↝ dom x ⟶
        A = sources (cs @ cs') s y ⟶ y ∉ Y) ∨ z ∉ A" and
      H: "c = ⟨Y⟩"
    have "y ∈ sources_aux cs' (run_flow cs s) x ∪
      ⋃ {sources cs' (run_flow cs s) y | y.
        run_flow cs' (run_flow cs s): dom y ↝ dom x ∧ y ∈ Y}"
      using D and H by simp
    hence "z ∈ sources_aux (cs @ cs') s x"
    using B and E and H proof (erule_tac UnE, blast)
      assume "y ∈ ⋃ {sources cs' (run_flow cs s) y | y.
        run_flow cs' (run_flow cs s): dom y ↝ dom x ∧ y ∈ Y}"
      then obtain w where
        I: "y ∈ sources cs' (run_flow cs s) w" and
        J: "run_flow cs' (run_flow cs s): dom w ↝ dom x" and
        K: "w ∈ Y"
        by blast
      have "z ∈ sources (cs @ cs') s w"
        using C and E and H and I by blast
      hence "w ∉ Y"
        using G and J by blast
      thus ?thesis
        using K by contradiction
    qed
  }
  ultimately show ?thesis
    by (simp only: append_assoc [symmetric] sources_aux.simps,
     auto simp: run_flow_append split: com_flow.split)
qed

lemma sources_member:
 "y ∈ sources cs' (run_flow cs s) x ⟹
    sources cs s y ⊆ sources (cs @ cs') s x"
and sources_aux_member:
 "y ∈ sources_aux cs' (run_flow cs s) x ⟹
    sources cs s y ⊆ sources_aux (cs @ cs') s x"
proof (induction cs' s x and cs' s x rule: sources_induct)
  fix cs' c s x
  show
   "⟦⋀z a. c = z ::= a ⟹ z = x ⟹
      y ∈ sources_aux cs' (run_flow cs s) x ⟹
        sources cs s y ⊆ sources_aux (cs @ cs') s x;
    ⋀z a b w. c = z ::= a ⟹ z = x ⟹
      y ∈ sources cs' (run_flow cs s) w ⟹
        sources cs s y ⊆ sources (cs @ cs') s w;
    ⋀z a. c = z ::= a ⟹ z ≠ x ⟹
      y ∈ sources cs' (run_flow cs s) x ⟹
        sources cs s y ⊆ sources (cs @ cs') s x;
    ⋀Y. c = ⟨Y⟩ ⟹
      y ∈ sources cs' (run_flow cs s) x ⟹
        sources cs s y ⊆ sources (cs @ cs') s x;
    ⋀Y a w. c = ⟨Y⟩ ⟹
      y ∈ sources cs' (run_flow cs s) w ⟹
        sources cs s y ⊆ sources (cs @ cs') s w;
    y ∈ sources (cs' @ [c]) (run_flow cs s) x⟧ ⟹
      sources cs s y ⊆ sources (cs @ cs' @ [c]) s x"
    by (auto, rule sources_member_1)
next
  fix cs' c s x
  show
   "⟦⋀z a. c = z ::= a ⟹
      y ∈ sources_aux cs' (run_flow cs s) x ⟹
        sources cs s y ⊆ sources_aux (cs @ cs') s x;
    ⋀Y. c = ⟨Y⟩ ⟹
      y ∈ sources_aux cs' (run_flow cs s) x ⟹
        sources cs s y ⊆ sources_aux (cs @ cs') s x;
    ⋀Y a w. c = ⟨Y⟩ ⟹
      y ∈ sources cs' (run_flow cs s) w ⟹
        sources cs s y ⊆ sources (cs @ cs') s w;
    y ∈ sources_aux (cs' @ [c]) (run_flow cs s) x⟧ ⟹
      sources cs s y ⊆ sources_aux (cs @ cs' @ [c]) s x"
    by (auto, rule sources_member_2)
qed simp_all


lemma ctyping2_confine:
 "⟦(c, s) ⇒ s'; (U, v) ⊨ c (⊆ A, X) = Some (B, Y);
    ∃(C, Z) ∈ U. ¬ C: dom ` Z ↝ {dom x}⟧ ⟹ s' x = s x"
by (induction arbitrary: A B X Y U v rule: big_step_induct,
 auto split: if_split_asm option.split_asm prod.split_asm, fastforce+)

lemma ctyping2_term_if:
 "⟦⋀x' y' z'' s. x' = x ⟹ y' = y ⟹ z = z'' ⟹ ∃s'. (c⇩1, s) ⇒ s';
    ⋀x' y' z'' s. x' = x ⟹ y' = y ⟹ z' = z'' ⟹ ∃s'. (c⇩2, s) ⇒ s'⟧ ⟹
  ∃s'. (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ s'"
by (cases "bval b s", fastforce+)

lemma ctyping2_term:
 "⟦(U, v) ⊨ c (⊆ A, X) = Some (B, Y);
    ∃(C, Z) ∈ U. ¬ C: dom ` Z ↝ UNIV⟧ ⟹ ∃s'. (c, s) ⇒ s'"
by (induction "(U, v)" c A X arbitrary: B Y U v s rule: ctyping2.induct,
 auto split: if_split_asm option.split_asm prod.split_asm, fastforce,
 erule ctyping2_term_if)


lemma ctyping2_correct_aux_skip [elim]:
 "⟦(SKIP, s) →*{cfs⇩1} (c⇩1, s⇩1); (c⇩1, s⇩1) →*{cfs⇩2} (c⇩2, s⇩2)⟧ ⟹
    (∀t⇩1. ∃c⇩2' t⇩2. ∀x.
      (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
        (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
      (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
    (∀x. (∃p ∈ U. case p of (B, W) ⇒
      ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶ no_upd (flow cfs⇩2) x)"
by (fastforce dest: small_stepsl_skip)

lemma ctyping2_correct_aux_assign [elim]:
  assumes
    A: "(if (∀s ∈ Univ? A X. ∀y ∈ avars a. s: dom y ↝ dom x) ∧
          (∀p ∈ U. ∀B Y. p = (B, Y) ⟶
            (∀s ∈ B. ∀y ∈ Y. s: dom y ↝ dom x))
        then Some (if x ∈ state ∧ A ≠ {}
          then if v ⊨ a (⊆ X)
            then ({s(x := aval a s) |s. s ∈ A}, insert x X)
            else (A, X - {x})
          else (A, Univ?? A X))
        else None) = Some (B, Y)"
      (is "(if ?P then _ else _) = _") and
    B: "(x ::= a, s) →*{cfs⇩1} (c⇩1, s⇩1)" and
    C: "(c⇩1, s⇩1) →*{cfs⇩2} (c⇩2, s⇩2)" and
    D: "r ∈ A" and
    E: "s = r (⊆ state ∩ X)"
  shows
   "(∀t⇩1. ∃c⇩2' t⇩2. ∀x.
      (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
        (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
      (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
    (∀x. (∃p ∈ U. case p of (B, Y) ⇒
      ∃s ∈ B. ∃y ∈ Y. ¬ s: dom y ↝ dom x) ⟶ no_upd (flow cfs⇩2) x)"
proof -
  have ?P
    using A by (simp split: if_split_asm)
  have F: "avars a ⊆ {y. s: dom y ↝ dom x}"
  proof (cases "state ⊆ X")
    case True
    with E have "interf s = interf r"
      by (blast intro: interf_state)
    with D and `?P` show ?thesis
      by (erule_tac conjE, drule_tac bspec, auto simp: univ_states_if_def)
  next
    case False
    with D and `?P` show ?thesis
      by (erule_tac conjE, drule_tac bspec, auto simp: univ_states_if_def)
  qed
  have "(c⇩1, s⇩1) = (x ::= a, s) ∨ (c⇩1, s⇩1) = (SKIP, s(x := aval a s))"
    using B by (blast dest: small_stepsl_assign)
  thus ?thesis
  proof
    assume "(c⇩1, s⇩1) = (x ::= a, s)"
    moreover from this have "(x ::= a, s) →*{cfs⇩2} (c⇩2, s⇩2)"
      using C by simp
    hence "(c⇩2, s⇩2) = (x ::= a, s) ∧ flow cfs⇩2 = [] ∨
      (c⇩2, s⇩2) = (SKIP, s(x := aval a s)) ∧ flow cfs⇩2 = [x ::= a]"
      by (rule small_stepsl_assign)
    moreover {
      fix t
      have "∃c' t'. ∀y.
        (y = x ⟶
          (s = t (⊆ sources_aux [x ::= a] s x) ⟶
            (x ::= a, t) →* (c', t') ∧ c' = SKIP) ∧
          (s = t (⊆ sources [x ::= a] s x) ⟶ aval a s = t' x)) ∧
        (y ≠ x ⟶
          (s = t (⊆ sources_aux [x ::= a] s y) ⟶
            (x ::= a, t) →* (c', t') ∧ c' = SKIP) ∧
          (s = t (⊆ sources [x ::= a] s y) ⟶ s y = t' y))"
      proof (rule exI [of _ SKIP], rule exI [of _ "t(x := aval a t)"])
        {
          assume "s = t (⊆ sources [x ::= a] s x)"
          hence "s = t (⊆ {y. s: dom y ↝ dom x ∧ y ∈ avars a})"
            by (subst (asm) append_Nil [symmetric],
             simp only: sources.simps, auto)
          hence "aval a s = aval a t"
            using F by (blast intro: avars_aval)
        }
        moreover {
          fix y
          assume "s = t (⊆ sources [x ::= a] s y)" and "y ≠ x"
          hence "s y = t y"
            by (subst (asm) append_Nil [symmetric],
             simp only: sources.simps, auto)
        }
        ultimately show "∀y.
          (y = x ⟶
            (s = t (⊆ sources_aux [x ::= a] s x) ⟶
              (x ::= a, t) →* (SKIP, t(x := aval a t)) ∧ SKIP = SKIP) ∧
            (s = t (⊆ sources [x ::= a] s x) ⟶
              aval a s = (t(x := aval a t)) x)) ∧
          (y ≠ x ⟶
            (s = t (⊆ sources_aux [x ::= a] s y) ⟶
              (x ::= a, t) →* (SKIP, t(x := aval a t)) ∧ SKIP = SKIP) ∧
            (s = t (⊆ sources [x ::= a] s y) ⟶
              s y = (t(x := aval a t)) y))"
          by simp
      qed
    }
    ultimately show ?thesis
      using `?P` by fastforce
  next
    assume "(c⇩1, s⇩1) = (SKIP, s(x := aval a s))"
    moreover from this have "(SKIP, s(x := aval a s)) →*{cfs⇩2} (c⇩2, s⇩2)"
      using C by simp
    hence "(c⇩2, s⇩2) = (SKIP, s(x := aval a s)) ∧ flow cfs⇩2 = []"
      by (rule small_stepsl_skip)
    ultimately show ?thesis
      by auto
  qed
qed

lemma ctyping2_correct_aux_seq:
  assumes
    A: "⋀B' s c' c'' s⇩1 s⇩2 cfs⇩1 cfs⇩2. B = B' ⟹
      ∃r ∈ A. s = r (⊆ state ∩ X) ⟹
        (c⇩1, s) →*{cfs⇩1} (c', s⇩1) ⟹ (c', s⇩1) →*{cfs⇩2} (c'', s⇩2) ⟹
          (∀t⇩1. ∃c⇩2' t⇩2. ∀x.
            (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
              (c', t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
            (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
          (∀x. (∃p ∈ U. case p of (B, W) ⇒
            ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
              no_upd (flow cfs⇩2) x)" and
    B: "⋀B' B'' C Z s c' c'' s⇩1 s⇩2 cfs⇩1 cfs⇩2. B = B' ⟹ B'' = B' ⟹
      (U, v) ⊨ c⇩2 (⊆ B', Y) = Some (C, Z) ⟹
        ∃r ∈ B'. s = r (⊆ state ∩ Y) ⟹
          (c⇩2, s) →*{cfs⇩1} (c', s⇩1) ⟹ (c', s⇩1) →*{cfs⇩2} (c'', s⇩2) ⟹
            (∀t⇩1. ∃c⇩2' t⇩2. ∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
                (c', t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
            (∀x. (∃p ∈ U. case p of (B, W) ⇒
              ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
                no_upd (flow cfs⇩2) x)" and
    C: "(U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y)" and
    D: "(U, v) ⊨ c⇩2 (⊆ B, Y) = Some (C, Z)" and
    E: "(c⇩1;; c⇩2, s) →*{cfs⇩1} (c', s⇩1)" and
    F: "(c', s⇩1) →*{cfs⇩2} (c'', s⇩2)" and
    G: "r ∈ A" and
    H: "s = r (⊆ state ∩ X)"
  shows
   "(∀t⇩1. ∃c⇩2' t⇩2. ∀x.
      (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
        (c', t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
      (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
    (∀x. (∃p ∈ U. case p of (B, W) ⇒
      ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶ no_upd (flow cfs⇩2) x)"
proof -
  have
   "(∃d' cfs. c' = d';; c⇩2 ∧
      (c⇩1, s) →*{cfs} (d', s⇩1)) ∨
    (∃s' cfs cfs'.
      (c⇩1, s) →*{cfs} (SKIP, s') ∧
      (c⇩2, s') →*{cfs'} (c', s⇩1))"
    using E by (blast dest: small_stepsl_seq)
  thus ?thesis
  proof (rule disjE, (erule_tac exE)+, (erule_tac [2] exE)+,
   erule_tac [!] conjE)
    fix d' cfs
    assume
      I: "c' = d';; c⇩2" and
      J: "(c⇩1, s) →*{cfs} (d', s⇩1)"
    hence "(d';; c⇩2, s⇩1) →*{cfs⇩2} (c'', s⇩2)"
      using F by simp
    hence
     "(∃d'' cfs'. c'' = d'';; c⇩2 ∧
        (d', s⇩1) →*{cfs'} (d'', s⇩2) ∧
        flow cfs⇩2 = flow cfs') ∨
      (∃s' cfs' cfs''.
        (d', s⇩1) →*{cfs'} (SKIP, s') ∧
        (c⇩2, s') →*{cfs''} (c'', s⇩2) ∧
        flow cfs⇩2 = flow cfs' @ flow cfs'')"
      by (blast dest: small_stepsl_seq)
    thus ?thesis
    proof (rule disjE, (erule_tac exE)+, (erule_tac [2] exE)+,
     (erule_tac [!] conjE)+)
      fix d'' cfs'
      assume "(d', s⇩1) →*{cfs'} (d'', s⇩2)"
      hence K:
       "(∀t⇩1. ∃c⇩2' t⇩2. ∀x.
          (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs') s⇩1 x) ⟶
            (d', t⇩1) →* (c⇩2', t⇩2) ∧ (d'' = SKIP) = (c⇩2' = SKIP)) ∧
          (s⇩1 = t⇩1 (⊆ sources (flow cfs') s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
        (∀x. (∃p ∈ U. case p of (B, W) ⇒
          ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶ no_upd (flow cfs') x)"
        using A [of B s cfs d' s⇩1 cfs' d'' s⇩2] and J and G and H by blast
      moreover assume "c'' = d'';; c⇩2" and "flow cfs⇩2 = flow cfs'"
      moreover {
        fix t⇩1
        obtain c⇩2' and t⇩2 where L: "∀x.
          (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs') s⇩1 x) ⟶
            (d', t⇩1) →* (c⇩2', t⇩2) ∧ (d'' = SKIP) = (c⇩2' = SKIP)) ∧
          (s⇩1 = t⇩1 (⊆ sources (flow cfs') s⇩1 x) ⟶ s⇩2 x = t⇩2 x)"
          using K by blast
        have "∃c⇩2' t⇩2. ∀x.
          (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs') s⇩1 x) ⟶
            (d';; c⇩2, t⇩1) →* (c⇩2', t⇩2) ∧ c⇩2' ≠ SKIP) ∧
          (s⇩1 = t⇩1 (⊆ sources (flow cfs') s⇩1 x) ⟶ s⇩2 x = t⇩2 x)"
        proof (rule exI [of _ "c⇩2';; c⇩2"], rule exI [of _ t⇩2])
          show "∀x.
            (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs') s⇩1 x) ⟶
              (d';; c⇩2, t⇩1) →* (c⇩2';; c⇩2, t⇩2) ∧ c⇩2';; c⇩2 ≠ SKIP) ∧
            (s⇩1 = t⇩1 (⊆ sources (flow cfs') s⇩1 x) ⟶ s⇩2 x = t⇩2 x)"
            using L by (auto intro: star_seq2)
        qed
      }
      ultimately show ?thesis
        using I by auto
    next
      fix s' cfs' cfs''
      assume
        K: "(d', s⇩1) →*{cfs'} (SKIP, s')" and
        L: "(c⇩2, s') →*{cfs''} (c'', s⇩2)"
      moreover have M: "s' = run_flow (flow cfs') s⇩1"
        using K by (rule small_stepsl_run_flow)
      ultimately have N:
       "(∀t⇩1. ∃c⇩2' t⇩2. ∀x.
          (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs') s⇩1 x) ⟶
            (d', t⇩1) →* (c⇩2', t⇩2) ∧ (SKIP = SKIP) = (c⇩2' = SKIP)) ∧
          (s⇩1 = t⇩1 (⊆ sources (flow cfs') s⇩1 x) ⟶
            run_flow (flow cfs') s⇩1 x = t⇩2 x)) ∧
        (∀x. (∃p ∈ U. case p of (B, W) ⇒
          ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶ no_upd (flow cfs') x)"
        using A [of B s cfs d' s⇩1 cfs' SKIP s'] and J and G and H by blast
      have O: "s⇩2 = run_flow (flow cfs'') s'"
        using L by (rule small_stepsl_run_flow)
      moreover have "(c⇩1, s) →*{cfs @ cfs'} (SKIP, s')"
        using J and K by (simp add: small_stepsl_append)
      hence "(c⇩1, s) ⇒ s'"
        by (auto dest: small_stepsl_steps simp: big_iff_small)
      hence "s' ∈ Univ B (⊆ state ∩ Y)"
        using C and G and H by (erule_tac ctyping2_approx, auto)
      ultimately have P:
       "(∀t⇩1. ∃c⇩2' t⇩2. ∀x.
          (run_flow (flow cfs') s⇩1 = t⇩1
            (⊆ sources_aux (flow cfs'') (run_flow (flow cfs') s⇩1) x) ⟶
              (c⇩2, t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
          (run_flow (flow cfs') s⇩1 = t⇩1
            (⊆ sources (flow cfs'') (run_flow (flow cfs') s⇩1) x) ⟶
              run_flow (flow cfs'') (run_flow (flow cfs') s⇩1) x = t⇩2 x)) ∧
        (∀x. (∃p ∈ U. case p of (B, W) ⇒
          ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶ no_upd (flow cfs'') x)"
        using B [of B B C Z s' "[]" c⇩2 s' cfs'' c'' s⇩2]
         and D and L and M by simp
      moreover assume "flow cfs⇩2 = flow cfs' @ flow cfs''"
      moreover {
        fix t⇩1
        obtain c⇩2' and t⇩2 where Q: "∀x.
          (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs') s⇩1 x) ⟶
            (d', t⇩1) →* (SKIP, t⇩2) ∧ (SKIP = SKIP) = (c⇩2' = SKIP)) ∧
          (s⇩1 = t⇩1 (⊆ sources (flow cfs') s⇩1 x) ⟶
            run_flow (flow cfs') s⇩1 x = t⇩2 x)"
          using N by blast
        obtain c⇩3' and t⇩3 where R: "∀x.
          (run_flow (flow cfs') s⇩1 = t⇩2
            (⊆ sources_aux (flow cfs'') (run_flow (flow cfs') s⇩1) x) ⟶
              (c⇩2, t⇩2) →* (c⇩3', t⇩3) ∧ (c'' = SKIP) = (c⇩3' = SKIP)) ∧
          (run_flow (flow cfs') s⇩1 = t⇩2
            (⊆ sources (flow cfs'') (run_flow (flow cfs') s⇩1) x) ⟶
              run_flow (flow cfs'') (run_flow (flow cfs') s⇩1) x = t⇩3 x)"
          using P by blast
        {
          fix x
          assume S: "s⇩1 = t⇩1
            (⊆ sources_aux (flow cfs' @ flow cfs'') s⇩1 x)"
          moreover have "sources_aux (flow cfs') s⇩1 x ⊆
            sources_aux (flow cfs' @ flow cfs'') s⇩1 x"
            by (rule sources_aux_append)
          ultimately have "(d', t⇩1) →* (SKIP, t⇩2)"
            using Q by blast
          hence "(d';; c⇩2, t⇩1) →* (SKIP;; c⇩2, t⇩2)"
            by (rule star_seq2)
          hence "(d';; c⇩2, t⇩1) →* (c⇩2, t⇩2)"
            by (blast intro: star_trans)
          moreover have "run_flow (flow cfs') s⇩1 = t⇩2
            (⊆ sources_aux (flow cfs'') (run_flow (flow cfs') s⇩1) x)"
          proof
            fix y
            assume "y ∈ sources_aux (flow cfs'')
              (run_flow (flow cfs') s⇩1) x"
            hence "sources (flow cfs') s⇩1 y ⊆
              sources_aux (flow cfs' @ flow cfs'') s⇩1 x"
              by (rule sources_aux_member)
            thus "run_flow (flow cfs') s⇩1 y = t⇩2 y"
              using Q and S by blast
          qed
          hence "(c⇩2, t⇩2) →* (c⇩3', t⇩3) ∧ (c'' = SKIP) = (c⇩3' = SKIP)"
            using R by simp
          ultimately have "(d';; c⇩2, t⇩1) →* (c⇩3', t⇩3) ∧
            (c'' = SKIP) = (c⇩3' = SKIP)"
            by (blast intro: star_trans)
        }
        moreover {
          fix x
          assume S: "s⇩1 = t⇩1
            (⊆ sources (flow cfs' @ flow cfs'') s⇩1 x)"
          have "run_flow (flow cfs') s⇩1 = t⇩2
            (⊆ sources (flow cfs'') (run_flow (flow cfs') s⇩1) x)"
          proof
            fix y
            assume "y ∈ sources (flow cfs'')
              (run_flow (flow cfs') s⇩1) x"
            hence "sources (flow cfs') s⇩1 y ⊆
              sources (flow cfs' @ flow cfs'') s⇩1 x"
              by (rule sources_member)
            thus "run_flow (flow cfs') s⇩1 y = t⇩2 y"
              using Q and S by blast
          qed
          hence "run_flow (flow cfs'') (run_flow (flow cfs') s⇩1) x = t⇩3 x"
            using R by simp
        }
        ultimately have "∃c⇩2' t⇩2. ∀x.
          (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs' @ flow cfs'') s⇩1 x) ⟶
            (d';; c⇩2, t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
          (s⇩1 = t⇩1 (⊆ sources (flow cfs' @ flow cfs'') s⇩1 x) ⟶
            run_flow (flow cfs'') (run_flow (flow cfs') s⇩1) x = t⇩2 x)"
          by auto
      }
      ultimately show ?thesis
        using I and N and M and O by (auto simp: no_upd_append)
    qed
  next
    fix s' cfs cfs'
    assume "(c⇩1, s) →*{cfs} (SKIP, s')"
    hence "(c⇩1, s) ⇒ s'"
      by (auto dest: small_stepsl_steps simp: big_iff_small)
    hence "s' ∈ Univ B (⊆ state ∩ Y)"
      using C and G and H by (erule_tac ctyping2_approx, auto)
    moreover assume "(c⇩2, s') →*{cfs'} (c', s⇩1)"
    ultimately show ?thesis
      using B [of B B C Z s' cfs' c' s⇩1 cfs⇩2 c'' s⇩2] and D and F by simp
  qed
qed

lemma ctyping2_correct_aux_if:
  assumes
    A: "⋀U' B C s c' c'' s⇩1 s⇩2 cfs⇩1 cfs⇩2.
      U' = insert (Univ? A X, bvars b) U ⟹ B = B⇩1 ⟹ C⇩1 = C ⟹
        ∃r ∈ B⇩1. s = r (⊆ state ∩ X) ⟹
          (c⇩1, s) →*{cfs⇩1} (c', s⇩1) ⟹ (c', s⇩1) →*{cfs⇩2} (c'', s⇩2) ⟹
            (∀t⇩1. ∃c⇩2' t⇩2. ∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
                (c', t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
            (∀x.
              ((∃s ∈ Univ? A X. ∃y ∈ bvars b. ¬ s: dom y ↝ dom x) ⟶
                no_upd (flow cfs⇩2) x) ∧
              ((∃p ∈ U. case p of (B, W) ⇒
                ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
                  no_upd (flow cfs⇩2) x))" and
    B: "⋀U' B C s c' c'' s⇩1 s⇩2 cfs⇩1 cfs⇩2.
      U' = insert (Univ? A X, bvars b) U ⟹ B = B⇩1 ⟹ C⇩2 = C ⟹
        ∃r ∈ B⇩2. s = r (⊆ state ∩ X) ⟹
          (c⇩2, s) →*{cfs⇩1} (c', s⇩1) ⟹ (c', s⇩1) →*{cfs⇩2} (c'', s⇩2) ⟹
            (∀t⇩1. ∃c⇩2' t⇩2. ∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
                (c', t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
            (∀x.
              ((∃s ∈ Univ? A X. ∃y ∈ bvars b. ¬ s: dom y ↝ dom x) ⟶
                no_upd (flow cfs⇩2) x) ∧
              ((∃p ∈ U. case p of (B, W) ⇒
                ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
                  no_upd (flow cfs⇩2) x))" and
    C: "⊨ b (⊆ A, X) = (B⇩1, B⇩2)" and
    D: "(insert (Univ? A X, bvars b) U, v) ⊨ c⇩1 (⊆ B⇩1, X) =
      Some (C⇩1, Y⇩1)" and
    E: "(insert (Univ? A X, bvars b) U, v) ⊨ c⇩2 (⊆ B⇩2, X) =
      Some (C⇩2, Y⇩2)" and
    F: "(IF b THEN c⇩1 ELSE c⇩2, s) →*{cfs⇩1} (c', s⇩1)" and
    G: "(c', s⇩1) →*{cfs⇩2} (c'', s⇩2)" and
    H: "r ∈ A" and
    I: "s = r (⊆ state ∩ X)"
  shows
   "(∀t⇩1. ∃c⇩2' t⇩2. ∀x.
      (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
    (c', t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
      (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
    (∀x. (∃p ∈ U. case p of (B, W) ⇒
      ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶ no_upd (flow cfs⇩2) x)"
proof -
  let ?U' = "insert (Univ? A X, bvars b) U"
  have J: "∀cs t x. s = t (⊆ sources_aux (⟨bvars b⟩ # cs) s x) ⟶
    bval b s ≠ bval b t ⟶ ¬ Univ? A X: dom ` bvars b ↝ {dom x}"
  proof (clarify del: notI)
    fix cs t x
    assume "s = t (⊆ sources_aux (⟨bvars b⟩ # cs) s x)"
    moreover assume "bval b s ≠ bval b t"
    hence "¬ s = t (⊆ bvars b)"
      by (erule_tac contrapos_nn, auto dest: bvars_bval)
    ultimately have "¬ (∀y ∈ bvars b. s: dom y ↝ dom x)"
      by (blast dest: sources_aux_observe_hd)
    moreover {
      fix r y
      assume "r ∈ A" and "y ∈ bvars b" and "¬ s: dom y ↝ dom x"
      moreover assume "state ⊆ X" and "s = r (⊆ state ∩ X)"
      hence "interf s = interf r"
        by (blast intro: interf_state)
      ultimately have "∃s ∈ A. ∃y ∈ bvars b. ¬ s: dom y ↝ dom x"
        by auto
    }
    ultimately show "¬ Univ? A X: dom ` bvars b ↝ {dom x}"
      using H and I by (auto simp: univ_states_if_def)
  qed
  have
   "(c', s⇩1) = (IF b THEN c⇩1 ELSE c⇩2, s) ∨
    bval b s ∧ (c⇩1, s) →*{tl cfs⇩1} (c', s⇩1) ∨
    ¬ bval b s ∧ (c⇩2, s) →*{tl cfs⇩1} (c', s⇩1)"
    using F by (blast dest: small_stepsl_if)
  thus ?thesis
  proof (rule disjE, erule_tac [2] disjE, erule_tac [2-3] conjE)
    assume K: "(c', s⇩1) = (IF b THEN c⇩1 ELSE c⇩2, s)"
    hence "(IF b THEN c⇩1 ELSE c⇩2, s) →*{cfs⇩2} (c'', s⇩2)"
      using G by simp
    hence
     "(c'', s⇩2) = (IF b THEN c⇩1 ELSE c⇩2, s) ∧
        flow cfs⇩2 = [] ∨
      bval b s ∧ (c⇩1, s) →*{tl cfs⇩2} (c'', s⇩2) ∧
        flow cfs⇩2 = ⟨bvars b⟩ # flow (tl cfs⇩2) ∨
      ¬ bval b s ∧ (c⇩2, s) →*{tl cfs⇩2} (c'', s⇩2) ∧
        flow cfs⇩2 = ⟨bvars b⟩ # flow (tl cfs⇩2)"
      by (rule small_stepsl_if)
    thus ?thesis
    proof (rule disjE, erule_tac [2] disjE, (erule_tac [2-3] conjE)+)
      assume "(c'', s⇩2) = (IF b THEN c⇩1 ELSE c⇩2, s) ∧ flow cfs⇩2 = []"
      thus ?thesis
        using K by auto
    next
      assume L: "bval b s"
      with C and H and I have "s ∈ Univ B⇩1 (⊆ state ∩ X)"
        by (drule_tac btyping2_approx [where s = s], auto)
      moreover assume M: "(c⇩1, s) →*{tl cfs⇩2} (c'', s⇩2)"
      moreover from this have N: "s⇩2 = run_flow (flow (tl cfs⇩2)) s"
        by (rule small_stepsl_run_flow)
      ultimately have O:
       "(∀t⇩1. ∃c⇩2' t⇩2. ∀x.
          (s = t⇩1 (⊆ sources_aux (flow (tl cfs⇩2)) s x) ⟶
            (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
          (s = t⇩1 (⊆ sources (flow (tl cfs⇩2)) s x) ⟶
            run_flow (flow (tl cfs⇩2)) s x = t⇩2 x)) ∧
        (∀x.
          ((∃s ∈ Univ? A X. ∃y ∈ bvars b. ¬ s: dom y ↝ dom x) ⟶
            no_upd (flow (tl cfs⇩2)) x) ∧
          ((∃p ∈ U. case p of (B, W) ⇒
            ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
              no_upd (flow (tl cfs⇩2)) x))"
        using A [of ?U' B⇩1 C⇩1 s "[]" c⇩1 s "tl cfs⇩2" c'' s⇩2] by simp
      moreover assume "flow cfs⇩2 = ⟨bvars b⟩ # flow (tl cfs⇩2)"
      moreover {
        fix t⇩1
        have "∃c⇩2' t⇩2. ∀x.
          (s = t⇩1 (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x) ⟶
            (IF b THEN c⇩1 ELSE c⇩2, t⇩1) →* (c⇩2', t⇩2) ∧
            (c'' = SKIP) = (c⇩2' = SKIP)) ∧
          (s = t⇩1 (⊆ sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x) ⟶
            run_flow (flow (tl cfs⇩2)) s x = t⇩2 x)"
        proof (cases "bval b t⇩1")
          case True
          hence P: "(IF b THEN c⇩1 ELSE c⇩2, t⇩1) → (c⇩1, t⇩1)" ..
          obtain c⇩2' and t⇩2 where Q: "∀x.
            (s = t⇩1 (⊆ sources_aux (flow (tl cfs⇩2)) s x) ⟶
              (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
            (s = t⇩1 (⊆ sources (flow (tl cfs⇩2)) s x) ⟶
              run_flow (flow (tl cfs⇩2)) s x = t⇩2 x)"
            using O by blast
          {
            fix x
            assume "s = t⇩1
              (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)"
            moreover have "sources_aux (flow (tl cfs⇩2)) s x ⊆
              sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x"
              by (rule sources_aux_observe_tl)
            ultimately have "(IF b THEN c⇩1 ELSE c⇩2, t⇩1) →* (c⇩2', t⇩2) ∧
              (c'' = SKIP) = (c⇩2' = SKIP)"
              using P and Q by (blast intro: star_trans)
          }
          moreover {
            fix x
            assume "s = t⇩1
              (⊆ sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)"
            moreover have "sources (flow (tl cfs⇩2)) s x ⊆
              sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x"
              by (rule sources_observe_tl)
            ultimately have "run_flow (flow (tl cfs⇩2)) s x = t⇩2 x"
              using Q by blast
          }
          ultimately show ?thesis
            by auto
        next
          assume P: "¬ bval b t⇩1"
          show ?thesis
          proof (cases "∃x. s = t⇩1
           (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)")
            from P have "(IF b THEN c⇩1 ELSE c⇩2, t⇩1) → (c⇩2, t⇩1)" ..
            moreover assume "∃x. s = t⇩1
              (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)"
            hence "∃x. ¬ Univ? A X: dom ` bvars b ↝ {dom x}"
              using J and L and P by blast
            then obtain t⇩2 where Q: "(c⇩2, t⇩1) ⇒ t⇩2"
              using E by (blast dest: ctyping2_term)
            hence "(c⇩2, t⇩1) →* (SKIP, t⇩2)"
              by (simp add: big_iff_small)
            ultimately have
              R: "(IF b THEN c⇩1 ELSE c⇩2, t⇩1) →* (SKIP, t⇩2)"
              by (blast intro: star_trans)
            show ?thesis
            proof (cases "c'' = SKIP")
              case True
              show ?thesis
              proof (rule exI [of _ SKIP], rule exI [of _ t⇩2])
                {
                  have "(IF b THEN c⇩1 ELSE c⇩2, t⇩1) →* (SKIP, t⇩2) ∧
                    (c'' = SKIP) = (SKIP = SKIP)"
                    using R and True by simp
                }
                moreover {
                  fix x
                  assume S: "s = t⇩1
                    (⊆ sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)"
                  moreover have
                   "sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x ⊆
                    sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x"
                    by (rule sources_aux_sources)
                  ultimately have "s = t⇩1
                    (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)"
                    by blast
                  hence T: "¬ Univ? A X: dom ` bvars b ↝ {dom x}"
                    using J and L and P by blast
                  hence U: "no_upd (⟨bvars b⟩ # flow (tl cfs⇩2)) x"
                    using O by simp
                  hence "run_flow (flow (tl cfs⇩2)) s x = s x"
                    by (simp add: no_upd_run_flow)
                  also from S and U have "… = t⇩1 x"
                    by (blast dest: no_upd_sources)
                  also from E and Q and T have "… = t⇩2 x"
                    by (drule_tac ctyping2_confine, auto)
                  finally have "run_flow (flow (tl cfs⇩2)) s x = t⇩2 x" .
                }
                ultimately show "∀x.
                  (s = t⇩1
                    (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x) ⟶
                      (IF b THEN c⇩1 ELSE c⇩2, t⇩1) →* (SKIP, t⇩2) ∧
                        (c'' = SKIP) = (SKIP = SKIP)) ∧
                  (s = t⇩1
                    (⊆ sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x) ⟶
                      run_flow (flow (tl cfs⇩2)) s x = t⇩2 x)"
                  by blast
              qed
            next
              case False
              show ?thesis
              proof (rule exI [of _ "IF b THEN c⇩1 ELSE c⇩2"],
               rule exI [of _ t⇩1])
                {
                  have "(IF b THEN c⇩1 ELSE c⇩2, t⇩1) →*
                    (IF b THEN c⇩1 ELSE c⇩2, t⇩1) ∧
                      (c'' = SKIP) = (IF b THEN c⇩1 ELSE c⇩2 = SKIP)"
                    using False by simp
                }
                moreover {
                  fix x
                  assume S: "s = t⇩1
                    (⊆ sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)"
                  moreover have
                   "sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x ⊆
                    sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x"
                    by (rule sources_aux_sources)
                  ultimately have "s = t⇩1
                    (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)"
                    by blast
                  hence "¬ Univ? A X: dom ` bvars b ↝ {dom x}"
                    using J and L and P by blast
                  hence T: "no_upd (⟨bvars b⟩ # flow (tl cfs⇩2)) x"
                    using O by simp
                  hence "run_flow (flow (tl cfs⇩2)) s x = s x"
                    by (simp add: no_upd_run_flow)
                  also have "… = t⇩1 x"
                    using S and T by (blast dest: no_upd_sources)
                  finally have "run_flow (flow (tl cfs⇩2)) s x = t⇩1 x" .
                }
                ultimately show "∀x.
                  (s = t⇩1
                    (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x) ⟶
                      (IF b THEN c⇩1 ELSE c⇩2, t⇩1) →*
                        (IF b THEN c⇩1 ELSE c⇩2, t⇩1) ∧
                          (c'' = SKIP) = (IF b THEN c⇩1 ELSE c⇩2 = SKIP)) ∧
                  (s = t⇩1
                    (⊆ sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x) ⟶
                      run_flow (flow (tl cfs⇩2)) s x = t⇩1 x)"
                  by blast
              qed
            qed
          qed blast
        qed
      }
      ultimately show ?thesis
        using K and N by auto
    next
      assume L: "¬ bval b s"
      with C and H and I have "s ∈ Univ B⇩2 (⊆ state ∩ X)"
        by (drule_tac btyping2_approx [where s = s], auto)
      moreover assume M: "(c⇩2, s) →*{tl cfs⇩2} (c'', s⇩2)"
      moreover from this have N: "s⇩2 = run_flow (flow (tl cfs⇩2)) s"
        by (rule small_stepsl_run_flow)
      ultimately have O:
       "(∀t⇩1. ∃c⇩2' t⇩2. ∀x.
          (s = t⇩1 (⊆ sources_aux (flow (tl cfs⇩2)) s x) ⟶
            (c⇩2, t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
          (s = t⇩1 (⊆ sources (flow (tl cfs⇩2)) s x) ⟶
            run_flow (flow (tl cfs⇩2)) s x = t⇩2 x)) ∧
        (∀x.
          ((∃s ∈ Univ? A X. ∃y ∈ bvars b. ¬ s: dom y ↝ dom x) ⟶
            no_upd (flow (tl cfs⇩2)) x) ∧
          ((∃p ∈ U. case p of (B, W) ⇒
            ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
              no_upd (flow (tl cfs⇩2)) x))"
        using B [of ?U' B⇩1 C⇩2 s "[]" c⇩2 s "tl cfs⇩2" c'' s⇩2] by simp
      moreover assume "flow cfs⇩2 = ⟨bvars b⟩ # flow (tl cfs⇩2)"
      moreover {
        fix t⇩1
        have "∃c⇩2' t⇩2. ∀x.
          (s = t⇩1 (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x) ⟶
            (IF b THEN c⇩1 ELSE c⇩2, t⇩1) →* (c⇩2', t⇩2) ∧
            (c'' = SKIP) = (c⇩2' = SKIP)) ∧
          (s = t⇩1 (⊆ sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x) ⟶
            run_flow (flow (tl cfs⇩2)) s x = t⇩2 x)"
        proof (cases "¬ bval b t⇩1")
          case True
          hence P: "(IF b THEN c⇩1 ELSE c⇩2, t⇩1) → (c⇩2, t⇩1)" ..
          obtain c⇩2' and t⇩2 where Q: "∀x.
            (s = t⇩1 (⊆ sources_aux (flow (tl cfs⇩2)) s x) ⟶
              (c⇩2, t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
            (s = t⇩1 (⊆ sources (flow (tl cfs⇩2)) s x) ⟶
              run_flow (flow (tl cfs⇩2)) s x = t⇩2 x)"
            using O by blast
          {
            fix x
            assume "s = t⇩1
              (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)"
            moreover have "sources_aux (flow (tl cfs⇩2)) s x ⊆
              sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x"
              by (rule sources_aux_observe_tl)
            ultimately have "(IF b THEN c⇩1 ELSE c⇩2, t⇩1) →* (c⇩2', t⇩2) ∧
              (c'' = SKIP) = (c⇩2' = SKIP)"
              using P and Q by (blast intro: star_trans)
          }
          moreover {
            fix x
            assume "s = t⇩1
              (⊆ sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)"
            moreover have "sources (flow (tl cfs⇩2)) s x ⊆
              sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x"
              by (rule sources_observe_tl)
            ultimately have "run_flow (flow (tl cfs⇩2)) s x = t⇩2 x"
              using Q by blast
          }
          ultimately show ?thesis
            by auto
        next
          case False
          hence P: "bval b t⇩1"
            by simp
          show ?thesis
          proof (cases "∃x. s = t⇩1
           (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)")
            from P have "(IF b THEN c⇩1 ELSE c⇩2, t⇩1) → (c⇩1, t⇩1)" ..
            moreover assume "∃x. s = t⇩1
              (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)"
            hence "∃x. ¬ Univ? A X: dom ` bvars b ↝ {dom x}"
              using J and L and P by blast
            then obtain t⇩2 where Q: "(c⇩1, t⇩1) ⇒ t⇩2"
              using D by (blast dest: ctyping2_term)
            hence "(c⇩1, t⇩1) →* (SKIP, t⇩2)"
              by (simp add: big_iff_small)
            ultimately have
              R: "(IF b THEN c⇩1 ELSE c⇩2, t⇩1) →* (SKIP, t⇩2)"
              by (blast intro: star_trans)
            show ?thesis
            proof (cases "c'' = SKIP")
              case True
              show ?thesis
              proof (rule exI [of _ SKIP], rule exI [of _ t⇩2])
                {
                  have "(IF b THEN c⇩1 ELSE c⇩2, t⇩1) →* (SKIP, t⇩2) ∧
                    (c'' = SKIP) = (SKIP = SKIP)"
                    using R and True by simp
                }
                moreover {
                  fix x
                  assume S: "s = t⇩1
                    (⊆ sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)"
                  moreover have
                   "sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x ⊆
                    sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x"
                    by (rule sources_aux_sources)
                  ultimately have "s = t⇩1
                    (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)"
                    by blast
                  hence T: "¬ Univ? A X: dom ` bvars b ↝ {dom x}"
                    using J and L and P by blast
                  hence U: "no_upd (⟨bvars b⟩ # flow (tl cfs⇩2)) x"
                    using O by simp
                  hence "run_flow (flow (tl cfs⇩2)) s x = s x"
                    by (simp add: no_upd_run_flow)
                  also from S and U have "… = t⇩1 x"
                    by (blast dest: no_upd_sources)
                  also from D and Q and T have "… = t⇩2 x"
                    by (drule_tac ctyping2_confine, auto)
                  finally have "run_flow (flow (tl cfs⇩2)) s x = t⇩2 x" .
                }
                ultimately show "∀x.
                  (s = t⇩1
                    (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x) ⟶
                      (IF b THEN c⇩1 ELSE c⇩2, t⇩1) →* (SKIP, t⇩2) ∧
                        (c'' = SKIP) = (SKIP = SKIP)) ∧
                  (s = t⇩1
                    (⊆ sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x) ⟶
                      run_flow (flow (tl cfs⇩2)) s x = t⇩2 x)"
                  by blast
              qed
            next
              case False
              show ?thesis
              proof (rule exI [of _ "IF b THEN c⇩1 ELSE c⇩2"],
               rule exI [of _ t⇩1])
                {
                  have "(IF b THEN c⇩1 ELSE c⇩2, t⇩1) →*
                    (IF b THEN c⇩1 ELSE c⇩2, t⇩1) ∧
                      (c'' = SKIP) = (IF b THEN c⇩1 ELSE c⇩2 = SKIP)"
                    using False by simp
                }
                moreover {
                  fix x
                  assume S: "s = t⇩1
                    (⊆ sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)"
                  moreover have
                   "sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x ⊆
                    sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x"
                    by (rule sources_aux_sources)
                  ultimately have "s = t⇩1
                    (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x)"
                    by blast
                  hence "¬ Univ? A X: dom ` bvars b ↝ {dom x}"
                    using J and L and P by blast
                  hence T: "no_upd (⟨bvars b⟩ # flow (tl cfs⇩2)) x"
                    using O by simp
                  hence "run_flow (flow (tl cfs⇩2)) s x = s x"
                    by (simp add: no_upd_run_flow)
                  also have "… = t⇩1 x"
                    using S and T by (blast dest: no_upd_sources)
                  finally have "run_flow (flow (tl cfs⇩2)) s x = t⇩1 x" .
                }
                ultimately show "∀x.
                  (s = t⇩1
                    (⊆ sources_aux (⟨bvars b⟩ # flow (tl cfs⇩2)) s x) ⟶
                      (IF b THEN c⇩1 ELSE c⇩2, t⇩1) →*
                        (IF b THEN c⇩1 ELSE c⇩2, t⇩1) ∧
                        (c'' = SKIP) = (IF b THEN c⇩1 ELSE c⇩2 = SKIP)) ∧
                  (s = t⇩1
                    (⊆ sources (⟨bvars b⟩ # flow (tl cfs⇩2)) s x) ⟶
                      run_flow (flow (tl cfs⇩2)) s x = t⇩1 x)"
                  by blast
              qed
            qed
          qed blast
        qed
      }
      ultimately show ?thesis
        using K and N by auto
    qed
  next
    assume "bval b s" and "(c⇩1, s) →*{tl cfs⇩1} (c', s⇩1)"
    moreover from this and C and H and I have "s ∈ Univ B⇩1 (⊆ state ∩ X)"
      by (drule_tac btyping2_approx [where s = s], auto)
    ultimately show ?thesis
      using A [of ?U' B⇩1 C⇩1 s "tl cfs⇩1" c' s⇩1 cfs⇩2 c'' s⇩2] and G by simp
  next
    assume "¬ bval b s" and "(c⇩2, s) →*{tl cfs⇩1} (c', s⇩1)"
    moreover from this and C and H and I have "s ∈ Univ B⇩2 (⊆ state ∩ X)"
      by (drule_tac btyping2_approx [where s = s], auto)
    ultimately show ?thesis
      using B [of ?U' B⇩1 C⇩2 s "tl cfs⇩1" c' s⇩1 cfs⇩2 c'' s⇩2] and G by simp
  qed
qed

lemma ctyping2_correct_aux_while:
  assumes
    A: "⋀B C' B' D' s c⇩1 c⇩2 s⇩1 s⇩2 cfs⇩1 cfs⇩2.
      B = B⇩1 ⟹ C' = C ⟹ B' = B⇩1' ⟹
      (∀s ∈ Univ? A X ∪ Univ? C Y. ∀x ∈ bvars b. All (interf s (dom x))) ∧
      (∀p ∈ U. case p of (B, W) ⇒ ∀s ∈ B. ∀x ∈ W. All (interf s (dom x))) ⟹
        D = D' ⟹ ∃r ∈ B⇩1. s = r (⊆ state ∩ X) ⟹
          (c, s) →*{cfs⇩1} (c⇩1, s⇩1) ⟹ (c⇩1, s⇩1) →*{cfs⇩2} (c⇩2, s⇩2) ⟹
            ∀t⇩1. ∃c⇩2' t⇩2. ∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
                (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)" and
    B: "⋀B C' B' D'' s c⇩1 c⇩2 s⇩1 s⇩2 cfs⇩1 cfs⇩2.
      B = B⇩1 ⟹ C' = C ⟹ B' = B⇩1' ⟹
      (∀s ∈ Univ? A X ∪ Univ? C Y. ∀x ∈ bvars b. All (interf s (dom x))) ∧
      (∀p ∈ U. case p of (B, W) ⇒ ∀s ∈ B. ∀x ∈ W. All (interf s (dom x))) ⟹
        D' = D'' ⟹ ∃r ∈ B⇩1'. s = r (⊆ state ∩ Y) ⟹
          (c, s) →*{cfs⇩1} (c⇩1, s⇩1) ⟹ (c⇩1, s⇩1) →*{cfs⇩2} (c⇩2, s⇩2) ⟹
            ∀t⇩1. ∃c⇩2' t⇩2. ∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
                (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)" and
    C: "(if (∀s ∈ Univ? A X ∪ Univ? C Y. ∀x ∈ bvars b. All (interf s (dom x))) ∧
      (∀p ∈ U. ∀B W. p = (B, W) ⟶ (∀s ∈ B. ∀x ∈ W. All (interf s (dom x))))
        then Some (B⇩2 ∪ B⇩2', Univ?? B⇩2 X ∩ Y) else None) = Some (B, W)" and
    D: "⊨ b (⊆ A, X) = (B⇩1, B⇩2)" and
    E: "⊢ c (⊆ B⇩1, X) = (C, Y)" and
    F: "⊨ b (⊆ C, Y) = (B⇩1', B⇩2')" and
    G: "({}, False) ⊨ c (⊆ B⇩1, X) = Some (D, Z)" and
    H: "({}, False) ⊨ c (⊆ B⇩1', Y) = Some (D', Z')"
  shows
   "⟦(WHILE b DO c, s) →*{cfs⇩1} (c⇩1, s⇩1);
      (c⇩1, s⇩1) →*{cfs⇩2} (c⇩2, s⇩2);
      s ∈ Univ A (⊆ state ∩ X) ∪ Univ C (⊆ state ∩ Y)⟧ ⟹
    (∀t⇩1. ∃c⇩2' t⇩2. ∀x.
      (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
        (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
      (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
    (∀x. (∃p ∈ U. case p of (B, W) ⇒
      ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶ no_upd (flow cfs⇩2) x)"
proof (induction "cfs⇩1 @ cfs⇩2" arbitrary: cfs⇩1 cfs⇩2 s c⇩1 s⇩1 rule: length_induct)
  fix cfs⇩1 cfs⇩2 s c⇩1 s⇩1
  assume
    I: "(WHILE b DO c, s) →*{cfs⇩1} (c⇩1, s⇩1)" and
    J: "(c⇩1, s⇩1) →*{cfs⇩2} (c⇩2, s⇩2)"
  assume "∀cfs. length cfs < length (cfs⇩1 @ cfs⇩2) ⟶
      (∀cfs⇩1 cfs⇩2. cfs = cfs⇩1 @ cfs⇩2 ⟶
        (∀s c⇩1 s⇩1. (WHILE b DO c, s) →*{cfs⇩1} (c⇩1, s⇩1) ⟶
          (c⇩1, s⇩1) →*{cfs⇩2} (c⇩2, s⇩2) ⟶
            s ∈ Univ A (⊆ state ∩ X) ∪ Univ C (⊆ state ∩ Y) ⟶
              (∀t⇩1. ∃c⇩2' t⇩2. ∀x.
                (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
                  (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
                (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
              (∀x. (∃(B, W) ∈ U. ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
                no_upd (flow cfs⇩2) x)))"
  note K = this [rule_format]
  assume L: "s ∈ Univ A (⊆ state ∩ X) ∪ Univ C (⊆ state ∩ Y)"
  moreover {
    fix s'
    assume "s ∈ Univ A (⊆ state ∩ X)" and "bval b s"
    hence N: "s ∈ Univ B⇩1 (⊆ state ∩ X)"
      using D by (drule_tac btyping2_approx, auto)
    assume "(c, s) ⇒ s'"
    hence "s' ∈ Univ D (⊆ state ∩ Z)"
      using G and N by (rule ctyping2_approx)
    moreover have "D ⊆ C ∧ Y ⊆ Z"
      using E and G by (rule ctyping1_ctyping2)
    ultimately have "s' ∈ Univ C (⊆ state ∩ Y)"
      by blast
  }
  moreover {
    fix s'
    assume "s ∈ Univ C (⊆ state ∩ Y)" and "bval b s"
    hence N: "s ∈ Univ B⇩1' (⊆ state ∩ Y)"
      using F by (drule_tac btyping2_approx, auto)
    assume "(c, s) ⇒ s'"
    hence "s' ∈ Univ D' (⊆ state ∩ Z')"
      using H and N by (rule ctyping2_approx)
    moreover obtain C' and Y' where O: "⊢ c (⊆ B⇩1', Y) = (C', Y')"
      by (cases "⊢ c (⊆ B⇩1', Y)", simp)
    hence "D' ⊆ C' ∧ Y' ⊆ Z'"
      using H by (rule ctyping1_ctyping2)
    ultimately have P: "s' ∈ Univ C' (⊆ state ∩ Y')"
      by blast
    have "⊢ c (⊆ C, Y) = (C, Y)"
      using E by (rule ctyping1_idem)
    moreover have "B⇩1' ⊆ C"
      using F by (blast dest: btyping2_un_eq)
    ultimately have "C' ⊆ C ∧ Y ⊆ Y'"
      by (metis order_refl ctyping1_mono O)
    hence "s' ∈ Univ C (⊆ state ∩ Y)"
      using P by blast
  }
  ultimately have M:
   "∀s'. (c, s) ⇒ s' ⟶ bval b s ⟶ s' ∈ Univ C (⊆ state ∩ Y)"
    by blast
  have N:
   "(∀s ∈ Univ? A X ∪ Univ? C Y. ∀x ∈ bvars b. All (interf s (dom x))) ∧
    (∀p ∈ U. ∀B W. p = (B, W) ⟶ (∀s ∈ B. ∀x ∈ W. All (interf s (dom x))))"
    using C by (simp split: if_split_asm)
  hence "∀cs x. (∃(B, Y) ∈ U.
    ∃s ∈ B. ∃y ∈ Y. ¬ s: dom y ↝ dom x) ⟶ no_upd cs x"
    by auto
  moreover {
    fix r t⇩1
    assume O: "r ∈ A" and P: "s = r (⊆ state ∩ X)"
    have Q: "∀x. ∀y ∈ bvars b. s: dom y ↝ dom x"
    proof (cases "state ⊆ X")
      case True
      with P have "interf s = interf r"
        by (blast intro: interf_state)
      with N and O show ?thesis
        by (erule_tac conjE, drule_tac bspec,
         auto simp: univ_states_if_def)
    next
      case False
      with N and O show ?thesis
        by (erule_tac conjE, drule_tac bspec,
         auto simp: univ_states_if_def)
    qed
    have "(c⇩1, s⇩1) = (WHILE b DO c, s) ∨
      (IF b THEN c;; WHILE b DO c ELSE SKIP, s) →*{tl cfs⇩1} (c⇩1, s⇩1)"
      using I by (blast dest: small_stepsl_while)
    hence "∃c⇩2' t⇩2. ∀x.
      (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
        (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
      (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)"
    proof
      assume R: "(c⇩1, s⇩1) = (WHILE b DO c, s)"
      hence "(WHILE b DO c, s) →*{cfs⇩2} (c⇩2, s⇩2)"
        using J by simp
      hence
       "(c⇩2, s⇩2) = (WHILE b DO c, s) ∧
          flow cfs⇩2 = [] ∨
        (IF b THEN c;; WHILE b DO c ELSE SKIP, s) →*{tl cfs⇩2} (c⇩2, s⇩2) ∧
          flow cfs⇩2 = flow (tl cfs⇩2)"
        (is "?P ∨ ?Q ∧ ?R")
        by (rule small_stepsl_while)
      thus ?thesis
      proof (rule disjE, erule_tac [2] conjE)
        assume ?P
        with R show ?thesis
          by auto
      next
        assume ?Q and ?R
        have
         "(c⇩2, s⇩2) = (IF b THEN c;; WHILE b DO c ELSE SKIP, s) ∧
            flow (tl cfs⇩2) = [] ∨
          bval b s ∧ (c;; WHILE b DO c, s) →*{tl2 cfs⇩2} (c⇩2, s⇩2) ∧
            flow (tl cfs⇩2) = ⟨bvars b⟩ # flow (tl2 cfs⇩2) ∨
          ¬ bval b s ∧ (SKIP, s) →*{tl2 cfs⇩2} (c⇩2, s⇩2) ∧
            flow (tl cfs⇩2) = ⟨bvars b⟩ # flow (tl2 cfs⇩2)"
          using `?Q` by (rule small_stepsl_if)
        thus ?thesis
        proof (erule_tac disjE, erule_tac [2] disjE, (erule_tac [2-3] conjE)+)
          assume "(c⇩2, s⇩2) = (IF b THEN c;; WHILE b DO c ELSE SKIP, s) ∧
            flow (tl cfs⇩2) = []"
          with R and `?R` show ?thesis
            by auto
        next
          assume S: "bval b s"
          with D and O and P have T: "s ∈ Univ B⇩1 (⊆ state ∩ X)"
            by (drule_tac btyping2_approx [where s = s], auto)
          assume U: "(c;; WHILE b DO c, s) →*{tl2 cfs⇩2} (c⇩2, s⇩2)"
          hence
           "(∃c' cfs. c⇩2 = c';; WHILE b DO c ∧
              (c, s) →*{cfs} (c', s⇩2) ∧
              flow (tl2 cfs⇩2) = flow cfs) ∨
            (∃s' cfs cfs'. length cfs' < length (tl2 cfs⇩2) ∧
              (c, s) →*{cfs} (SKIP, s') ∧
              (WHILE b DO c, s') →*{cfs'} (c⇩2, s⇩2) ∧
              flow (tl2 cfs⇩2) = flow cfs @ flow cfs')"
            by (rule small_stepsl_seq)
          moreover assume "flow (tl cfs⇩2) = ⟨bvars b⟩ # flow (tl2 cfs⇩2)"
          moreover have "s⇩2 = run_flow (flow (tl2 cfs⇩2)) s"
            using U by (rule small_stepsl_run_flow)
          moreover {
            fix c' cfs
            assume "(c, s) →*{cfs} (c', run_flow (flow cfs) s)"
            then obtain c⇩2' and t⇩2 where V: "∀x.
              (s = t⇩1 (⊆ sources_aux (flow cfs) s x) ⟶
                (c, t⇩1) →* (c⇩2', t⇩2) ∧ (c' = SKIP) = (c⇩2' = SKIP)) ∧
              (s = t⇩1 (⊆ sources (flow cfs) s x) ⟶
                run_flow (flow cfs) s x = t⇩2 x)"
              using A [of B⇩1 C B⇩1' D s "[]" c s cfs c'
               "run_flow (flow cfs) s"] and N and T by force
            {
              fix x
              assume W: "s = t⇩1 (⊆ sources_aux (⟨bvars b⟩ # flow cfs) s x)"
              moreover have "sources_aux (flow cfs) s x ⊆
                sources_aux (⟨bvars b⟩ # (flow cfs)) s x"
                by (rule sources_aux_observe_tl)
              ultimately have "(c, t⇩1) →* (c⇩2', t⇩2)"
                using V by blast
              hence "(c;; WHILE b DO c, t⇩1) →* (c⇩2';; WHILE b DO c, t⇩2)"
                by (rule star_seq2)
              moreover have "s = t⇩1 (⊆ bvars b)"
                using Q and W by (blast dest: sources_aux_observe_hd)
              hence "bval b t⇩1"
                using S by (blast dest: bvars_bval)
              hence "(WHILE b DO c, t⇩1) →* (c;; WHILE b DO c, t⇩1)"
                by (blast intro: star_trans)
              ultimately have "(WHILE b DO c, t⇩1) →*
               (c⇩2';; WHILE b DO c, t⇩2) ∧ c⇩2';; WHILE b DO c ≠ SKIP"
                by (blast intro: star_trans)
            }
            moreover {
              fix x
              assume "s = t⇩1 (⊆ sources (⟨bvars b⟩ # flow cfs) s x)"
              moreover have "sources (flow cfs) s x ⊆
                sources (⟨bvars b⟩ # (flow cfs)) s x"
                by (rule sources_observe_tl)
              ultimately have "run_flow (flow cfs) s x = t⇩2 x"
                using V by blast
            }
            ultimately have "∃c⇩2' t⇩2. ∀x.
              (s = t⇩1 (⊆ sources_aux (⟨bvars b⟩ # flow cfs) s x) ⟶
                (WHILE b DO c, t⇩1) →* (c⇩2', t⇩2) ∧ c⇩2' ≠ SKIP) ∧
              (s = t⇩1 (⊆ sources (⟨bvars b⟩ # flow cfs) s x) ⟶
                run_flow (flow cfs) s x = t⇩2 x)"
              by blast
          }
          moreover {
            fix s' cfs cfs'
            assume
              V: "length cfs' < length cfs⇩2 - Suc (Suc 0)" and
              W: "(c, s) →*{cfs} (SKIP, s')" and
              X: "(WHILE b DO c, s') →*{cfs'}
                (c⇩2, run_flow (flow cfs') (run_flow (flow cfs) s))"
            then obtain c⇩2' and t⇩2 where "∀x.
              (s = t⇩1 (⊆ sources_aux (flow cfs) s x) ⟶
                (c, t⇩1) →* (c⇩2', t⇩2) ∧ (SKIP = SKIP) = (c⇩2' = SKIP)) ∧
              (s = t⇩1 (⊆ sources (flow cfs) s x) ⟶ s' x = t⇩2 x)"
              using A [of B⇩1 C B⇩1' D s "[]" c s cfs SKIP s']
               and N and T by force
            moreover have Y: "s' = run_flow (flow cfs) s"
              using W by (rule small_stepsl_run_flow)
            ultimately have Z: "∀x.
              (s = t⇩1 (⊆ sources_aux (flow cfs) s x) ⟶
                (c, t⇩1) →* (SKIP, t⇩2)) ∧
              (s = t⇩1 (⊆ sources (flow cfs) s x) ⟶
                run_flow (flow cfs) s x = t⇩2 x)"
              by blast
            assume "s⇩2 = run_flow (flow cfs') (run_flow (flow cfs) s)"
            moreover have "(c, s) ⇒ s'"
              using W by (auto dest: small_stepsl_steps simp: big_iff_small)
            hence "s' ∈ Univ C (⊆ state ∩ Y)"
              using M and S by blast
            ultimately obtain c⇩3' and t⇩3 where AA: "∀x.
              (run_flow (flow cfs) s = t⇩2
                (⊆ sources_aux (flow cfs') (run_flow (flow cfs) s) x) ⟶
                  (WHILE b DO c, t⇩2) →* (c⇩3', t⇩3) ∧
                  (c⇩2 = SKIP) = (c⇩3' = SKIP)) ∧
              (run_flow (flow cfs) s = t⇩2
                (⊆ sources (flow cfs') (run_flow (flow cfs) s) x) ⟶
                  run_flow (flow cfs') (run_flow (flow cfs) s) x = t⇩3 x)"
              using K [of cfs' "[]" cfs' s' "WHILE b DO c" s']
               and V and X and Y by force
            {
              fix x
              assume AB: "s = t⇩1
                (⊆ sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x)"
              moreover have "sources_aux (flow cfs) s x ⊆
                sources_aux (flow cfs @ flow cfs') s x"
                by (rule sources_aux_append)
              moreover have AC: "sources_aux (flow cfs @ flow cfs') s x ⊆
                sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                by (rule sources_aux_observe_tl)
              ultimately have "(c, t⇩1) →* (SKIP, t⇩2)"
                using Z by blast
              hence "(c;; WHILE b DO c, t⇩1) →* (SKIP;; WHILE b DO c, t⇩2)"
                by (rule star_seq2)
              moreover have "s = t⇩1 (⊆ bvars b)"
                using Q and AB by (blast dest: sources_aux_observe_hd)
              hence "bval b t⇩1"
                using S by (blast dest: bvars_bval)
              hence "(WHILE b DO c, t⇩1) →* (c;; WHILE b DO c, t⇩1)"
                by (blast intro: star_trans)
              ultimately have "(WHILE b DO c, t⇩1) →* (WHILE b DO c, t⇩2)"
                by (blast intro: star_trans)
              moreover have "run_flow (flow cfs) s = t⇩2
                (⊆ sources_aux (flow cfs') (run_flow (flow cfs) s) x)"
              proof
                fix y
                assume "y ∈ sources_aux (flow cfs')
                  (run_flow (flow cfs) s) x"
                hence "sources (flow cfs) s y ⊆
                  sources_aux (flow cfs @ flow cfs') s x"
                  by (rule sources_aux_member)
                hence "sources (flow cfs) s y ⊆
                  sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                  using AC by simp
                thus "run_flow (flow cfs) s y = t⇩2 y"
                  using Z and AB by blast
              qed
              hence "(WHILE b DO c, t⇩2) →* (c⇩3', t⇩3) ∧
                (c⇩2 = SKIP) = (c⇩3' = SKIP)"
                using AA by simp
              ultimately have "(WHILE b DO c, t⇩1) →* (c⇩3', t⇩3) ∧
                (c⇩2 = SKIP) = (c⇩3' = SKIP)"
                by (blast intro: star_trans)
            }
            moreover {
              fix x
              assume AB: "s = t⇩1
                (⊆ sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x)"
              have "run_flow (flow cfs) s = t⇩2
                (⊆ sources (flow cfs') (run_flow (flow cfs) s) x)"
              proof
                fix y
                assume "y ∈ sources (flow cfs')
                  (run_flow (flow cfs) s) x"
                hence "sources (flow cfs) s y ⊆
                  sources (flow cfs @ flow cfs') s x"
                  by (rule sources_member)
                moreover have "sources (flow cfs @ flow cfs') s x ⊆
                  sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                  by (rule sources_observe_tl)
                ultimately have "sources (flow cfs) s y ⊆
                  sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                  by simp
                thus "run_flow (flow cfs) s y = t⇩2 y"
                  using Z and AB by blast
              qed
              hence "run_flow (flow cfs') (run_flow (flow cfs) s) x = t⇩3 x"
                using AA by simp
            }
            ultimately have "∃c⇩3' t⇩3. ∀x.
              (s = t⇩1
                (⊆ sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x) ⟶
                  (WHILE b DO c, t⇩1) →* (c⇩3', t⇩3) ∧
                  (c⇩2 = SKIP) = (c⇩3' = SKIP)) ∧
              (s = t⇩1
                (⊆ sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x) ⟶
                  run_flow (flow cfs') (run_flow (flow cfs) s) x = t⇩3 x)"
              by auto
          }
          ultimately show ?thesis
            using R and `?R` by (auto simp: run_flow_append)
        next
          assume
            S: "¬ bval b s" and
            T: "flow (tl cfs⇩2) = ⟨bvars b⟩ # flow (tl2 cfs⇩2)"
          moreover assume "(SKIP, s) →*{tl2 cfs⇩2} (c⇩2, s⇩2)"
          hence U: "(c⇩2, s⇩2) = (SKIP, s) ∧ flow (tl2 cfs⇩2) = []"
            by (rule small_stepsl_skip)
          show ?thesis
          proof (rule exI [of _ SKIP], rule exI [of _ t⇩1])
            {
              fix x
              have "(WHILE b DO c, t⇩1) →
                (IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1)" ..
              moreover assume "s = t⇩1 (⊆ sources_aux [⟨bvars b⟩] s x)"
              hence "s = t⇩1 (⊆ bvars b)"
                using Q by (blast dest: sources_aux_observe_hd)
              hence "¬ bval b t⇩1"
                using S by (blast dest: bvars_bval)
              hence "(IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →
                (SKIP, t⇩1)" ..
              ultimately have "(WHILE b DO c, t⇩1) →* (SKIP, t⇩1)"
                by (blast intro: star_trans)
            }
            moreover {
              fix x
              assume "s = t⇩1 (⊆ sources [⟨bvars b⟩] s x)"
              hence "s x = t⇩1 x"
                by (subst (asm) append_Nil [symmetric],
                 simp only: sources.simps, auto)
            }
            ultimately show "∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
                (c⇩1, t⇩1) →* (SKIP, t⇩1) ∧ (c⇩2 = SKIP) = (SKIP = SKIP)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩1 x)"
              using R and T and U and `?R` by auto
          qed
        qed
      qed
    next
      assume "(IF b THEN c;; WHILE b DO c ELSE SKIP, s) →*{tl cfs⇩1} (c⇩1, s⇩1)"
      hence
       "(c⇩1, s⇩1) = (IF b THEN c;; WHILE b DO c ELSE SKIP, s) ∧
          flow (tl cfs⇩1) = [] ∨
        bval b s ∧ (c;; WHILE b DO c, s) →*{tl2 cfs⇩1} (c⇩1, s⇩1) ∧
          flow (tl cfs⇩1) = ⟨bvars b⟩ # flow (tl2 cfs⇩1) ∨
        ¬ bval b s ∧ (SKIP, s) →*{tl2 cfs⇩1} (c⇩1, s⇩1) ∧
          flow (tl cfs⇩1) = ⟨bvars b⟩ # flow (tl2 cfs⇩1)"
        by (rule small_stepsl_if)
      thus ?thesis
      proof (rule disjE, erule_tac [2] disjE, erule_tac conjE,
       (erule_tac [2-3] conjE)+)
        assume R: "(c⇩1, s⇩1) = (IF b THEN c;; WHILE b DO c ELSE SKIP, s)"
        hence "(IF b THEN c;; WHILE b DO c ELSE SKIP, s) →*{cfs⇩2} (c⇩2, s⇩2)"
          using J by simp
        hence
         "(c⇩2, s⇩2) = (IF b THEN c;; WHILE b DO c ELSE SKIP, s) ∧
            flow cfs⇩2 = [] ∨
          bval b s ∧ (c;; WHILE b DO c, s) →*{tl cfs⇩2} (c⇩2, s⇩2) ∧
            flow cfs⇩2 = ⟨bvars b⟩ # flow (tl cfs⇩2) ∨
          ¬ bval b s ∧ (SKIP, s) →*{tl cfs⇩2} (c⇩2, s⇩2) ∧
            flow cfs⇩2 = ⟨bvars b⟩ # flow (tl cfs⇩2)"
          by (rule small_stepsl_if)
        thus ?thesis
        proof (erule_tac disjE, erule_tac [2] disjE, (erule_tac [2-3] conjE)+)
          assume "(c⇩2, s⇩2) = (IF b THEN c;; WHILE b DO c ELSE SKIP, s) ∧
            flow cfs⇩2 = []"
          with R show ?thesis
            by auto
        next
          assume S: "bval b s"
          with D and O and P have T: "s ∈ Univ B⇩1 (⊆ state ∩ X)"
            by (drule_tac btyping2_approx [where s = s], auto)
          assume U: "(c;; WHILE b DO c, s) →*{tl cfs⇩2} (c⇩2, s⇩2)"
          hence
           "(∃c' cfs. c⇩2 = c';; WHILE b DO c ∧
              (c, s) →*{cfs} (c', s⇩2) ∧
              flow (tl cfs⇩2) = flow cfs) ∨
            (∃s' cfs cfs'. length cfs' < length (tl cfs⇩2) ∧
              (c, s) →*{cfs} (SKIP, s') ∧
              (WHILE b DO c, s') →*{cfs'} (c⇩2, s⇩2) ∧
              flow (tl cfs⇩2) = flow cfs @ flow cfs')"
            by (rule small_stepsl_seq)
          moreover assume "flow cfs⇩2 = ⟨bvars b⟩ # flow (tl cfs⇩2)"
          moreover have "s⇩2 = run_flow (flow (tl cfs⇩2)) s"
            using U by (rule small_stepsl_run_flow)
          moreover {
            fix c' cfs
            assume "(c, s) →*{cfs} (c', run_flow (flow cfs) s)"
            then obtain c⇩2' and t⇩2 where V: "∀x.
              (s = t⇩1 (⊆ sources_aux (flow cfs) s x) ⟶
                (c, t⇩1) →* (c⇩2', t⇩2) ∧ (c' = SKIP) = (c⇩2' = SKIP)) ∧
              (s = t⇩1 (⊆ sources (flow cfs) s x) ⟶
                run_flow (flow cfs) s x = t⇩2 x)"
              using A [of B⇩1 C B⇩1' D s "[]" c s cfs c'
               "run_flow (flow cfs) s"] and N and T by force
            {
              fix x
              assume W: "s = t⇩1 (⊆ sources_aux (⟨bvars b⟩ # flow cfs) s x)"
              moreover have "sources_aux (flow cfs) s x ⊆
                sources_aux (⟨bvars b⟩ # (flow cfs)) s x"
                by (rule sources_aux_observe_tl)
              ultimately have "(c, t⇩1) →* (c⇩2', t⇩2)"
                using V by blast
              hence "(c;; WHILE b DO c, t⇩1) →* (c⇩2';; WHILE b DO c, t⇩2)"
                by (rule star_seq2)
              moreover have "s = t⇩1 (⊆ bvars b)"
                using Q and W by (blast dest: sources_aux_observe_hd)
              hence "bval b t⇩1"
                using S by (blast dest: bvars_bval)
              hence "(IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →
                (c;; WHILE b DO c, t⇩1)" ..
              ultimately have
               "(IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →*
                  (c⇩2';; WHILE b DO c, t⇩2) ∧ c⇩2';; WHILE b DO c ≠ SKIP"
                by (blast intro: star_trans)
            }
            moreover {
              fix x
              assume "s = t⇩1 (⊆ sources (⟨bvars b⟩ # flow cfs) s x)"
              moreover have "sources (flow cfs) s x ⊆
                sources (⟨bvars b⟩ # (flow cfs)) s x"
                by (rule sources_observe_tl)
              ultimately have "run_flow (flow cfs) s x = t⇩2 x"
                using V by blast
            }
            ultimately have "∃c⇩2' t⇩2. ∀x.
              (s = t⇩1 (⊆ sources_aux (⟨bvars b⟩ # flow cfs) s x) ⟶
                (IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →* (c⇩2', t⇩2) ∧
                  c⇩2' ≠ SKIP) ∧
              (s = t⇩1 (⊆ sources (⟨bvars b⟩ # flow cfs) s x) ⟶
                run_flow (flow cfs) s x = t⇩2 x)"
              by blast
          }
          moreover {
            fix s' cfs cfs'
            assume
              V: "length cfs' < length cfs⇩2 - Suc 0" and
              W: "(c, s) →*{cfs} (SKIP, s')" and
              X: "(WHILE b DO c, s') →*{cfs'}
                (c⇩2, run_flow (flow cfs') (run_flow (flow cfs) s))"
            then obtain c⇩2' and t⇩2 where "∀x.
              (s = t⇩1 (⊆ sources_aux (flow cfs) s x) ⟶
                (c, t⇩1) →* (c⇩2', t⇩2) ∧ (SKIP = SKIP) = (c⇩2' = SKIP)) ∧
              (s = t⇩1 (⊆ sources (flow cfs) s x) ⟶ s' x = t⇩2 x)"
              using A [of B⇩1 C B⇩1' D s "[]" c s cfs SKIP s']
               and N and T by force
            moreover have Y: "s' = run_flow (flow cfs) s"
              using W by (rule small_stepsl_run_flow)
            ultimately have Z: "∀x.
              (s = t⇩1 (⊆ sources_aux (flow cfs) s x) ⟶
                (c, t⇩1) →* (SKIP, t⇩2)) ∧
              (s = t⇩1 (⊆ sources (flow cfs) s x) ⟶
                run_flow (flow cfs) s x = t⇩2 x)"
              by blast
            assume "s⇩2 = run_flow (flow cfs') (run_flow (flow cfs) s)"
            moreover have "(c, s) ⇒ s'"
              using W by (auto dest: small_stepsl_steps simp: big_iff_small)
            hence "s' ∈ Univ C (⊆ state ∩ Y)"
              using M and S by blast
            ultimately obtain c⇩3' and t⇩3 where AA: "∀x.
              (run_flow (flow cfs) s = t⇩2
                (⊆ sources_aux (flow cfs') (run_flow (flow cfs) s) x) ⟶
                  (WHILE b DO c, t⇩2) →* (c⇩3', t⇩3) ∧
                  (c⇩2 = SKIP) = (c⇩3' = SKIP)) ∧
              (run_flow (flow cfs) s = t⇩2
                (⊆ sources (flow cfs') (run_flow (flow cfs) s) x) ⟶
                  run_flow (flow cfs') (run_flow (flow cfs) s) x = t⇩3 x)"
              using K [of cfs' "[]" cfs' s' "WHILE b DO c" s']
               and V and X and Y by force
            {
              fix x
              assume AB: "s = t⇩1
                (⊆ sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x)"
              moreover have "sources_aux (flow cfs) s x ⊆
                sources_aux (flow cfs @ flow cfs') s x"
                by (rule sources_aux_append)
              moreover have AC: "sources_aux (flow cfs @ flow cfs') s x ⊆
                sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                by (rule sources_aux_observe_tl)
              ultimately have "(c, t⇩1) →* (SKIP, t⇩2)"
                using Z by blast
              hence "(c;; WHILE b DO c, t⇩1) →* (SKIP;; WHILE b DO c, t⇩2)"
                by (rule star_seq2)
              moreover have "s = t⇩1 (⊆ bvars b)"
                using Q and AB by (blast dest: sources_aux_observe_hd)
              hence "bval b t⇩1"
                using S by (blast dest: bvars_bval)
              hence "(IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →
                (c;; WHILE b DO c, t⇩1)" ..
              ultimately have "(IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →*
                (WHILE b DO c, t⇩2)"
                by (blast intro: star_trans)
              moreover have "run_flow (flow cfs) s = t⇩2
                (⊆ sources_aux (flow cfs') (run_flow (flow cfs) s) x)"
              proof
                fix y
                assume "y ∈ sources_aux (flow cfs')
                  (run_flow (flow cfs) s) x"
                hence "sources (flow cfs) s y ⊆
                  sources_aux (flow cfs @ flow cfs') s x"
                  by (rule sources_aux_member)
                hence "sources (flow cfs) s y ⊆
                  sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                  using AC by simp
                thus "run_flow (flow cfs) s y = t⇩2 y"
                  using Z and AB by blast
              qed
              hence "(WHILE b DO c, t⇩2) →* (c⇩3', t⇩3) ∧
                (c⇩2 = SKIP) = (c⇩3' = SKIP)"
                using AA by simp
              ultimately have
               "(IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →*
                  (c⇩3', t⇩3) ∧ (c⇩2 = SKIP) = (c⇩3' = SKIP)"
                by (blast intro: star_trans)
            }
            moreover {
              fix x
              assume AB: "s = t⇩1
                (⊆ sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x)"
              have "run_flow (flow cfs) s = t⇩2
                (⊆ sources (flow cfs') (run_flow (flow cfs) s) x)"
              proof
                fix y
                assume "y ∈ sources (flow cfs')
                  (run_flow (flow cfs) s) x"
                hence "sources (flow cfs) s y ⊆
                  sources (flow cfs @ flow cfs') s x"
                  by (rule sources_member)
                moreover have "sources (flow cfs @ flow cfs') s x ⊆
                  sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                  by (rule sources_observe_tl)
                ultimately have "sources (flow cfs) s y ⊆
                  sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                  by simp
                thus "run_flow (flow cfs) s y = t⇩2 y"
                  using Z and AB by blast
              qed
              hence "run_flow (flow cfs') (run_flow (flow cfs) s) x = t⇩3 x"
                using AA by simp
            }
            ultimately have "∃c⇩3' t⇩3. ∀x.
              (s = t⇩1
                (⊆ sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x) ⟶
                  (IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →* (c⇩3', t⇩3) ∧
                  (c⇩2 = SKIP) = (c⇩3' = SKIP)) ∧
              (s = t⇩1
                (⊆ sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x) ⟶
                  run_flow (flow cfs') (run_flow (flow cfs) s) x = t⇩3 x)"
              by auto
          }
          ultimately show ?thesis
            using R by (auto simp: run_flow_append)
        next
          assume
            S: "¬ bval b s" and
            T: "flow cfs⇩2 = ⟨bvars b⟩ # flow (tl cfs⇩2)"
          assume "(SKIP, s) →*{tl cfs⇩2} (c⇩2, s⇩2)"
          hence U: "(c⇩2, s⇩2) = (SKIP, s) ∧ flow (tl cfs⇩2) = []"
            by (rule small_stepsl_skip)
          show ?thesis
          proof (rule exI [of _ SKIP], rule exI [of _ t⇩1])
            {
              fix x
              assume "s = t⇩1 (⊆ sources_aux [⟨bvars b⟩] s x)"
              hence "s = t⇩1 (⊆ bvars b)"
                using Q by (blast dest: sources_aux_observe_hd)
              hence "¬ bval b t⇩1"
                using S by (blast dest: bvars_bval)
              hence "(IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →
                (SKIP, t⇩1)" ..
            }
            moreover {
              fix x
              assume "s = t⇩1 (⊆ sources [⟨bvars b⟩] s x)"
              hence "s x = t⇩1 x"
                by (subst (asm) append_Nil [symmetric],
                 simp only: sources.simps, auto)
            }
            ultimately show "∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
                (c⇩1, t⇩1) →* (SKIP, t⇩1) ∧ (c⇩2 = SKIP) = (SKIP = SKIP)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩1 x)"
              using R and T and U by auto
          qed
        qed
      next
        assume R: "bval b s"
        with D and O and P have S: "s ∈ Univ B⇩1 (⊆ state ∩ X)"
          by (drule_tac btyping2_approx [where s = s], auto)
        assume "(c;; WHILE b DO c, s) →*{tl2 cfs⇩1} (c⇩1, s⇩1)"
        hence
         "(∃c' cfs'. c⇩1 = c';; WHILE b DO c ∧
            (c, s) →*{cfs'} (c', s⇩1) ∧
            flow (tl2 cfs⇩1) = flow cfs') ∨
          (∃s' cfs' cfs''. length cfs'' < length (tl2 cfs⇩1) ∧
            (c, s) →*{cfs'} (SKIP, s') ∧
            (WHILE b DO c, s') →*{cfs''} (c⇩1, s⇩1) ∧
            flow (tl2 cfs⇩1) = flow cfs' @ flow cfs'')"
          by (rule small_stepsl_seq)
        moreover {
          fix c' cfs
          assume
            T: "(c, s) →*{cfs} (c', s⇩1)" and
            U: "c⇩1 = c';; WHILE b DO c"
          hence V: "(c';; WHILE b DO c, s⇩1) →*{cfs⇩2} (c⇩2, s⇩2)"
            using J by simp
          hence W: "s⇩2 = run_flow (flow cfs⇩2) s⇩1"
            by (rule small_stepsl_run_flow)
          have
           "(∃c'' cfs'. c⇩2 = c'';; WHILE b DO c ∧
              (c', s⇩1) →*{cfs'} (c'', s⇩2) ∧
              flow cfs⇩2 = flow cfs') ∨
            (∃s' cfs' cfs''. length cfs'' < length cfs⇩2 ∧
              (c', s⇩1) →*{cfs'} (SKIP, s') ∧
              (WHILE b DO c, s') →*{cfs''} (c⇩2, s⇩2) ∧
              flow cfs⇩2 = flow cfs' @ flow cfs'')"
            using V by (rule small_stepsl_seq)
          moreover {
            fix c'' cfs'
            assume "(c', s⇩1) →*{cfs'} (c'', s⇩2)"
            then obtain c⇩2' and t⇩2 where X: "∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs') s⇩1 x) ⟶
                (c', t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs') s⇩1 x) ⟶
                run_flow (flow cfs⇩2) s⇩1 x = t⇩2 x)"
              using A [of B⇩1 C B⇩1' D s cfs c' s⇩1 cfs' c''
               "run_flow (flow cfs⇩2) s⇩1"] and N and S and T and W by force
            assume
              Y: "c⇩2 = c'';; WHILE b DO c" and
              Z: "flow cfs⇩2 = flow cfs'"
            have ?thesis
            proof (rule exI [of _ "c⇩2';; WHILE b DO c"], rule exI [of _ t⇩2])
              from U and W and X and Y and Z show "∀x.
                (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
                  (c⇩1, t⇩1) →* (c⇩2';; WHILE b DO c, t⇩2) ∧
                    (c⇩2 = SKIP) = (c⇩2';; WHILE b DO c = SKIP)) ∧
                (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)"
                by (auto intro: star_seq2)
            qed
          }
          moreover {
            fix s' cfs' cfs''
            assume
              X: "length cfs'' < length cfs⇩2" and
              Y: "(c', s⇩1) →*{cfs'} (SKIP, s')" and
              Z: "(WHILE b DO c, s') →*{cfs''} (c⇩2, s⇩2)"
            then obtain c⇩2' and t⇩2 where "∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs') s⇩1 x) ⟶
                (c', t⇩1) →* (c⇩2', t⇩2) ∧ (SKIP = SKIP) = (c⇩2' = SKIP)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs') s⇩1 x) ⟶ s' x = t⇩2 x)"
              using A [of B⇩1 C B⇩1' D s cfs c' s⇩1 cfs' SKIP s']
               and N and S and T by force
            moreover have AA: "s' = run_flow (flow cfs') s⇩1"
              using Y by (rule small_stepsl_run_flow)
            ultimately have AB: "∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs') s⇩1 x) ⟶
                (c', t⇩1) →* (SKIP, t⇩2)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs') s⇩1 x) ⟶
                run_flow (flow cfs') s⇩1 x = t⇩2 x)"
              by blast
            have AC: "s⇩2 = run_flow (flow cfs'') s'"
              using Z by (rule small_stepsl_run_flow)
            moreover have "(c, s) →*{cfs @ cfs'} (SKIP, s')"
              using T and Y by (simp add: small_stepsl_append)
            hence "(c, s) ⇒ s'"
              by (auto dest: small_stepsl_steps simp: big_iff_small)
            hence "s' ∈ Univ C (⊆ state ∩ Y)"
              using M and R by blast
            ultimately obtain c⇩2' and t⇩3 where AD: "∀x.
              (run_flow (flow cfs') s⇩1 = t⇩2
                (⊆ sources_aux (flow cfs'') (run_flow (flow cfs') s⇩1) x) ⟶
                  (WHILE b DO c, t⇩2) →* (c⇩2', t⇩3) ∧
                  (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
              (run_flow (flow cfs') s⇩1 = t⇩2
                (⊆ sources (flow cfs'') (run_flow (flow cfs') s⇩1) x) ⟶
                  run_flow (flow cfs'') (run_flow (flow cfs') s⇩1) x = t⇩3 x)"
              using K [of cfs'' "[]" cfs'' s' "WHILE b DO c" s']
               and X and Z and AA by force
            moreover assume "flow cfs⇩2 = flow cfs' @ flow cfs''"
            moreover {
              fix x
              assume AE: "s⇩1 = t⇩1
                (⊆ sources_aux (flow cfs' @ flow cfs'') s⇩1 x)"
              moreover have "sources_aux (flow cfs') s⇩1 x ⊆
                sources_aux (flow cfs' @ flow cfs'') s⇩1 x"
                by (rule sources_aux_append)
              ultimately have "(c', t⇩1) →* (SKIP, t⇩2)"
                using AB by blast
              hence "(c';; WHILE b DO c, t⇩1) →* (SKIP;; WHILE b DO c, t⇩2)"
                by (rule star_seq2)
              hence "(c';; WHILE b DO c, t⇩1) →* (WHILE b DO c, t⇩2)"
                by (blast intro: star_trans)
              moreover have "run_flow (flow cfs') s⇩1 = t⇩2
                (⊆ sources_aux (flow cfs'') (run_flow (flow cfs') s⇩1) x)"
              proof
                fix y
                assume "y ∈ sources_aux (flow cfs'')
                  (run_flow (flow cfs') s⇩1) x"
                hence "sources (flow cfs') s⇩1 y ⊆
                  sources_aux (flow cfs' @ flow cfs'') s⇩1 x"
                  by (rule sources_aux_member)
                thus "run_flow (flow cfs') s⇩1 y = t⇩2 y"
                  using AB and AE by blast
              qed
              hence "(WHILE b DO c, t⇩2) →* (c⇩2', t⇩3) ∧
                (c⇩2 = SKIP) = (c⇩2' = SKIP)"
                using AD by simp
              ultimately have "(c';; WHILE b DO c, t⇩1) →* (c⇩2', t⇩3) ∧
                (c⇩2 = SKIP) = (c⇩2' = SKIP)"
                by (blast intro: star_trans)
            }
            moreover {
              fix x
              assume AE: "s⇩1 = t⇩1
                (⊆ sources (flow cfs' @ flow cfs'') s⇩1 x)"
              have "run_flow (flow cfs') s⇩1 = t⇩2
                (⊆ sources (flow cfs'') (run_flow (flow cfs') s⇩1) x)"
              proof
                fix y
                assume "y ∈ sources (flow cfs'')
                  (run_flow (flow cfs') s⇩1) x"
                hence "sources (flow cfs') s⇩1 y ⊆
                  sources (flow cfs' @ flow cfs'') s⇩1 x"
                  by (rule sources_member)
                thus "run_flow (flow cfs') s⇩1 y = t⇩2 y"
                  using AB and AE by blast
              qed
              hence "run_flow (flow cfs'')
                (run_flow (flow cfs') s⇩1) x = t⇩3 x"
                using AD by simp
            }
            ultimately have ?thesis
              by (metis U AA AC)
          }
          ultimately have ?thesis
            by blast
        }
        moreover {
          fix s' cfs cfs'
          assume
           "length cfs' < length (tl2 cfs⇩1)" and
           "(c, s) →*{cfs} (SKIP, s')" and
           "(WHILE b DO c, s') →*{cfs'} (c⇩1, s⇩1)"
          moreover from this have "(c, s) ⇒ s'"
            by (auto dest: small_stepsl_steps simp: big_iff_small)
          hence "s' ∈ Univ C (⊆ state ∩ Y)"
            using M and R by blast
          ultimately have ?thesis
            using K [of "cfs' @ cfs⇩2" cfs' cfs⇩2 s' c⇩1 s⇩1] and J by force
        }
        ultimately show ?thesis
          by blast
      next
        assume "(SKIP, s) →*{tl2 cfs⇩1} (c⇩1, s⇩1)"
        hence "(c⇩1, s⇩1) = (SKIP, s)"
          by (blast dest: small_stepsl_skip)
        moreover from this have "(c⇩2, s⇩2) = (SKIP, s) ∧ flow cfs⇩2 = []"
          using J by (blast dest: small_stepsl_skip)
        ultimately show ?thesis
          by auto
      qed
    qed
  }
  moreover {
    fix r t⇩1
    assume O: "r ∈ C" and P: "s = r (⊆ state ∩ Y)"
    have Q: "∀x. ∀y ∈ bvars b. s: dom y ↝ dom x"
    proof (cases "state ⊆ Y")
      case True
      with P have "interf s = interf r"
        by (blast intro: interf_state)
      with N and O show ?thesis
        by (erule_tac conjE, drule_tac bspec,
         auto simp: univ_states_if_def)
    next
      case False
      with N and O show ?thesis
        by (erule_tac conjE, drule_tac bspec,
         auto simp: univ_states_if_def)
    qed
    have "(c⇩1, s⇩1) = (WHILE b DO c, s) ∨
      (IF b THEN c;; WHILE b DO c ELSE SKIP, s) →*{tl cfs⇩1} (c⇩1, s⇩1)"
      using I by (blast dest: small_stepsl_while)
    hence "∃c⇩2' t⇩2. ∀x.
      (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
        (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
      (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)"
    proof
      assume R: "(c⇩1, s⇩1) = (WHILE b DO c, s)"
      hence "(WHILE b DO c, s) →*{cfs⇩2} (c⇩2, s⇩2)"
        using J by simp
      hence
       "(c⇩2, s⇩2) = (WHILE b DO c, s) ∧
          flow cfs⇩2 = [] ∨
        (IF b THEN c;; WHILE b DO c ELSE SKIP, s) →*{tl cfs⇩2} (c⇩2, s⇩2) ∧
          flow cfs⇩2 = flow (tl cfs⇩2)"
        (is "?P ∨ ?Q ∧ ?R")
        by (rule small_stepsl_while)
      thus ?thesis
      proof (rule disjE, erule_tac [2] conjE)
        assume ?P
        with R show ?thesis
          by auto
      next
        assume ?Q and ?R
        have
         "(c⇩2, s⇩2) = (IF b THEN c;; WHILE b DO c ELSE SKIP, s) ∧
            flow (tl cfs⇩2) = [] ∨
          bval b s ∧ (c;; WHILE b DO c, s) →*{tl2 cfs⇩2} (c⇩2, s⇩2) ∧
            flow (tl cfs⇩2) = ⟨bvars b⟩ # flow (tl2 cfs⇩2) ∨
          ¬ bval b s ∧ (SKIP, s) →*{tl2 cfs⇩2} (c⇩2, s⇩2) ∧
            flow (tl cfs⇩2) = ⟨bvars b⟩ # flow (tl2 cfs⇩2)"
          using `?Q` by (rule small_stepsl_if)
        thus ?thesis
        proof (erule_tac disjE, erule_tac [2] disjE, (erule_tac [2-3] conjE)+)
          assume "(c⇩2, s⇩2) = (IF b THEN c;; WHILE b DO c ELSE SKIP, s) ∧
            flow (tl cfs⇩2) = []"
          with R and `?R` show ?thesis
            by auto
        next
          assume S: "bval b s"
          with F and O and P have T: "s ∈ Univ B⇩1' (⊆ state ∩ Y)"
            by (drule_tac btyping2_approx [where s = s], auto)
          assume U: "(c;; WHILE b DO c, s) →*{tl2 cfs⇩2} (c⇩2, s⇩2)"
          hence
           "(∃c' cfs. c⇩2 = c';; WHILE b DO c ∧
              (c, s) →*{cfs} (c', s⇩2) ∧
              flow (tl2 cfs⇩2) = flow cfs) ∨
            (∃s' cfs cfs'. length cfs' < length (tl2 cfs⇩2) ∧
              (c, s) →*{cfs} (SKIP, s') ∧
              (WHILE b DO c, s') →*{cfs'} (c⇩2, s⇩2) ∧
              flow (tl2 cfs⇩2) = flow cfs @ flow cfs')"
            by (rule small_stepsl_seq)
          moreover assume "flow (tl cfs⇩2) = ⟨bvars b⟩ # flow (tl2 cfs⇩2)"
          moreover have "s⇩2 = run_flow (flow (tl2 cfs⇩2)) s"
            using U by (rule small_stepsl_run_flow)
          moreover {
            fix c' cfs
            assume "(c, s) →*{cfs} (c', run_flow (flow cfs) s)"
            then obtain c⇩2' and t⇩2 where V: "∀x.
              (s = t⇩1 (⊆ sources_aux (flow cfs) s x) ⟶
                (c, t⇩1) →* (c⇩2', t⇩2) ∧ (c' = SKIP) = (c⇩2' = SKIP)) ∧
              (s = t⇩1 (⊆ sources (flow cfs) s x) ⟶
                run_flow (flow cfs) s x = t⇩2 x)"
              using B [of B⇩1 C B⇩1' D' s "[]" c s cfs c'
               "run_flow (flow cfs) s"] and N and T by force
            {
              fix x
              assume W: "s = t⇩1 (⊆ sources_aux (⟨bvars b⟩ # flow cfs) s x)"
              moreover have "sources_aux (flow cfs) s x ⊆
                sources_aux (⟨bvars b⟩ # (flow cfs)) s x"
                by (rule sources_aux_observe_tl)
              ultimately have "(c, t⇩1) →* (c⇩2', t⇩2)"
                using V by blast
              hence "(c;; WHILE b DO c, t⇩1) →* (c⇩2';; WHILE b DO c, t⇩2)"
                by (rule star_seq2)
              moreover have "s = t⇩1 (⊆ bvars b)"
                using Q and W by (blast dest: sources_aux_observe_hd)
              hence "bval b t⇩1"
                using S by (blast dest: bvars_bval)
              hence "(WHILE b DO c, t⇩1) →* (c;; WHILE b DO c, t⇩1)"
                by (blast intro: star_trans)
              ultimately have "(WHILE b DO c, t⇩1) →*
               (c⇩2';; WHILE b DO c, t⇩2) ∧ c⇩2';; WHILE b DO c ≠ SKIP"
                by (blast intro: star_trans)
            }
            moreover {
              fix x
              assume "s = t⇩1 (⊆ sources (⟨bvars b⟩ # flow cfs) s x)"
              moreover have "sources (flow cfs) s x ⊆
                sources (⟨bvars b⟩ # (flow cfs)) s x"
                by (rule sources_observe_tl)
              ultimately have "run_flow (flow cfs) s x = t⇩2 x"
                using V by blast
            }
            ultimately have "∃c⇩2' t⇩2. ∀x.
              (s = t⇩1 (⊆ sources_aux (⟨bvars b⟩ # flow cfs) s x) ⟶
                (WHILE b DO c, t⇩1) →* (c⇩2', t⇩2) ∧ c⇩2' ≠ SKIP) ∧
              (s = t⇩1 (⊆ sources (⟨bvars b⟩ # flow cfs) s x) ⟶
                run_flow (flow cfs) s x = t⇩2 x)"
              by blast
          }
          moreover {
            fix s' cfs cfs'
            assume
              V: "length cfs' < length cfs⇩2 - Suc (Suc 0)" and
              W: "(c, s) →*{cfs} (SKIP, s')" and
              X: "(WHILE b DO c, s') →*{cfs'}
                (c⇩2, run_flow (flow cfs') (run_flow (flow cfs) s))"
            then obtain c⇩2' and t⇩2 where "∀x.
              (s = t⇩1 (⊆ sources_aux (flow cfs) s x) ⟶
                (c, t⇩1) →* (c⇩2', t⇩2) ∧ (SKIP = SKIP) = (c⇩2' = SKIP)) ∧
              (s = t⇩1 (⊆ sources (flow cfs) s x) ⟶ s' x = t⇩2 x)"
              using B [of B⇩1 C B⇩1' D' s "[]" c s cfs SKIP s']
               and N and T by force
            moreover have Y: "s' = run_flow (flow cfs) s"
              using W by (rule small_stepsl_run_flow)
            ultimately have Z: "∀x.
              (s = t⇩1 (⊆ sources_aux (flow cfs) s x) ⟶
                (c, t⇩1) →* (SKIP, t⇩2)) ∧
              (s = t⇩1 (⊆ sources (flow cfs) s x) ⟶
                run_flow (flow cfs) s x = t⇩2 x)"
              by blast
            assume "s⇩2 = run_flow (flow cfs') (run_flow (flow cfs) s)"
            moreover have "(c, s) ⇒ s'"
              using W by (auto dest: small_stepsl_steps simp: big_iff_small)
            hence "s' ∈ Univ C (⊆ state ∩ Y)"
              using M and S by blast
            ultimately obtain c⇩3' and t⇩3 where AA: "∀x.
              (run_flow (flow cfs) s = t⇩2
                (⊆ sources_aux (flow cfs') (run_flow (flow cfs) s) x) ⟶
                  (WHILE b DO c, t⇩2) →* (c⇩3', t⇩3) ∧
                  (c⇩2 = SKIP) = (c⇩3' = SKIP)) ∧
              (run_flow (flow cfs) s = t⇩2
                (⊆ sources (flow cfs') (run_flow (flow cfs) s) x) ⟶
                  run_flow (flow cfs') (run_flow (flow cfs) s) x = t⇩3 x)"
              using K [of cfs' "[]" cfs' s' "WHILE b DO c" s']
               and V and X and Y by force
            {
              fix x
              assume AB: "s = t⇩1
                (⊆ sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x)"
              moreover have "sources_aux (flow cfs) s x ⊆
                sources_aux (flow cfs @ flow cfs') s x"
                by (rule sources_aux_append)
              moreover have AC: "sources_aux (flow cfs @ flow cfs') s x ⊆
                sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                by (rule sources_aux_observe_tl)
              ultimately have "(c, t⇩1) →* (SKIP, t⇩2)"
                using Z by blast
              hence "(c;; WHILE b DO c, t⇩1) →* (SKIP;; WHILE b DO c, t⇩2)"
                by (rule star_seq2)
              moreover have "s = t⇩1 (⊆ bvars b)"
                using Q and AB by (blast dest: sources_aux_observe_hd)
              hence "bval b t⇩1"
                using S by (blast dest: bvars_bval)
              hence "(WHILE b DO c, t⇩1) →* (c;; WHILE b DO c, t⇩1)"
                by (blast intro: star_trans)
              ultimately have "(WHILE b DO c, t⇩1) →* (WHILE b DO c, t⇩2)"
                by (blast intro: star_trans)
              moreover have "run_flow (flow cfs) s = t⇩2
                (⊆ sources_aux (flow cfs') (run_flow (flow cfs) s) x)"
              proof
                fix y
                assume "y ∈ sources_aux (flow cfs')
                  (run_flow (flow cfs) s) x"
                hence "sources (flow cfs) s y ⊆
                  sources_aux (flow cfs @ flow cfs') s x"
                  by (rule sources_aux_member)
                hence "sources (flow cfs) s y ⊆
                  sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                  using AC by simp
                thus "run_flow (flow cfs) s y = t⇩2 y"
                  using Z and AB by blast
              qed
              hence "(WHILE b DO c, t⇩2) →* (c⇩3', t⇩3) ∧
                (c⇩2 = SKIP) = (c⇩3' = SKIP)"
                using AA by simp
              ultimately have "(WHILE b DO c, t⇩1) →* (c⇩3', t⇩3) ∧
                (c⇩2 = SKIP) = (c⇩3' = SKIP)"
                by (blast intro: star_trans)
            }
            moreover {
              fix x
              assume AB: "s = t⇩1
                (⊆ sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x)"
              have "run_flow (flow cfs) s = t⇩2
                (⊆ sources (flow cfs') (run_flow (flow cfs) s) x)"
              proof
                fix y
                assume "y ∈ sources (flow cfs')
                  (run_flow (flow cfs) s) x"
                hence "sources (flow cfs) s y ⊆
                  sources (flow cfs @ flow cfs') s x"
                  by (rule sources_member)
                moreover have "sources (flow cfs @ flow cfs') s x ⊆
                  sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                  by (rule sources_observe_tl)
                ultimately have "sources (flow cfs) s y ⊆
                  sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                  by simp
                thus "run_flow (flow cfs) s y = t⇩2 y"
                  using Z and AB by blast
              qed
              hence "run_flow (flow cfs') (run_flow (flow cfs) s) x = t⇩3 x"
                using AA by simp
            }
            ultimately have "∃c⇩3' t⇩3. ∀x.
              (s = t⇩1
                (⊆ sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x) ⟶
                  (WHILE b DO c, t⇩1) →* (c⇩3', t⇩3) ∧
                  (c⇩2 = SKIP) = (c⇩3' = SKIP)) ∧
              (s = t⇩1
                (⊆ sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x) ⟶
                  run_flow (flow cfs') (run_flow (flow cfs) s) x = t⇩3 x)"
              by auto
          }
          ultimately show ?thesis
            using R and `?R` by (auto simp: run_flow_append)
        next
          assume
            S: "¬ bval b s" and
            T: "flow (tl cfs⇩2) = ⟨bvars b⟩ # flow (tl2 cfs⇩2)"
          assume "(SKIP, s) →*{tl2 cfs⇩2} (c⇩2, s⇩2)"
          hence U: "(c⇩2, s⇩2) = (SKIP, s) ∧ flow (tl2 cfs⇩2) = []"
            by (rule small_stepsl_skip)
          show ?thesis
          proof (rule exI [of _ SKIP], rule exI [of _ t⇩1])
            {
              fix x
              have "(WHILE b DO c, t⇩1) →
                (IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1)" ..
              moreover assume "s = t⇩1 (⊆ sources_aux [⟨bvars b⟩] s x)"
              hence "s = t⇩1 (⊆ bvars b)"
                using Q by (blast dest: sources_aux_observe_hd)
              hence "¬ bval b t⇩1"
                using S by (blast dest: bvars_bval)
              hence "(IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →
                (SKIP, t⇩1)" ..
              ultimately have "(WHILE b DO c, t⇩1) →* (SKIP, t⇩1)"
                by (blast intro: star_trans)
            }
            moreover {
              fix x
              assume "s = t⇩1 (⊆ sources [⟨bvars b⟩] s x)"
              hence "s x = t⇩1 x"
                by (subst (asm) append_Nil [symmetric],
                 simp only: sources.simps, auto)
            }
            ultimately show "∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
                (c⇩1, t⇩1) →* (SKIP, t⇩1) ∧ (c⇩2 = SKIP) = (SKIP = SKIP)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩1 x)"
              using R and T and U and `?R` by auto
          qed
        qed
      qed
    next
      assume "(IF b THEN c;; WHILE b DO c ELSE SKIP, s) →*{tl cfs⇩1} (c⇩1, s⇩1)"
      hence
       "(c⇩1, s⇩1) = (IF b THEN c;; WHILE b DO c ELSE SKIP, s) ∧
          flow (tl cfs⇩1) = [] ∨
        bval b s ∧ (c;; WHILE b DO c, s) →*{tl2 cfs⇩1} (c⇩1, s⇩1) ∧
          flow (tl cfs⇩1) = ⟨bvars b⟩ # flow (tl2 cfs⇩1) ∨
        ¬ bval b s ∧ (SKIP, s) →*{tl2 cfs⇩1} (c⇩1, s⇩1) ∧
          flow (tl cfs⇩1) = ⟨bvars b⟩ # flow (tl2 cfs⇩1)"
        by (rule small_stepsl_if)
      thus ?thesis
      proof (rule disjE, erule_tac [2] disjE, erule_tac conjE,
       (erule_tac [2-3] conjE)+)
        assume R: "(c⇩1, s⇩1) = (IF b THEN c;; WHILE b DO c ELSE SKIP, s)"
        hence "(IF b THEN c;; WHILE b DO c ELSE SKIP, s) →*{cfs⇩2} (c⇩2, s⇩2)"
          using J by simp
        hence
         "(c⇩2, s⇩2) = (IF b THEN c;; WHILE b DO c ELSE SKIP, s) ∧
            flow cfs⇩2 = [] ∨
          bval b s ∧ (c;; WHILE b DO c, s) →*{tl cfs⇩2} (c⇩2, s⇩2) ∧
            flow cfs⇩2 = ⟨bvars b⟩ # flow (tl cfs⇩2) ∨
          ¬ bval b s ∧ (SKIP, s) →*{tl cfs⇩2} (c⇩2, s⇩2) ∧
            flow cfs⇩2 = ⟨bvars b⟩ # flow (tl cfs⇩2)"
          by (rule small_stepsl_if)
        thus ?thesis
        proof (erule_tac disjE, erule_tac [2] disjE, (erule_tac [2-3] conjE)+)
          assume "(c⇩2, s⇩2) = (IF b THEN c;; WHILE b DO c ELSE SKIP, s) ∧
            flow cfs⇩2 = []"
          with R show ?thesis
            by auto
        next
          assume S: "bval b s"
          with F and O and P have T: "s ∈ Univ B⇩1' (⊆ state ∩ Y)"
            by (drule_tac btyping2_approx [where s = s], auto)
          assume U: "(c;; WHILE b DO c, s) →*{tl cfs⇩2} (c⇩2, s⇩2)"
          hence
           "(∃c' cfs. c⇩2 = c';; WHILE b DO c ∧
              (c, s) →*{cfs} (c', s⇩2) ∧
              flow (tl cfs⇩2) = flow cfs) ∨
            (∃s' cfs cfs'. length cfs' < length (tl cfs⇩2) ∧
              (c, s) →*{cfs} (SKIP, s') ∧
              (WHILE b DO c, s') →*{cfs'} (c⇩2, s⇩2) ∧
              flow (tl cfs⇩2) = flow cfs @ flow cfs')"
            by (rule small_stepsl_seq)
          moreover assume "flow cfs⇩2 = ⟨bvars b⟩ # flow (tl cfs⇩2)"
          moreover have "s⇩2 = run_flow (flow (tl cfs⇩2)) s"
            using U by (rule small_stepsl_run_flow)
          moreover {
            fix c' cfs
            assume "(c, s) →*{cfs} (c', run_flow (flow cfs) s)"
            then obtain c⇩2' and t⇩2 where V: "∀x.
              (s = t⇩1 (⊆ sources_aux (flow cfs) s x) ⟶
                (c, t⇩1) →* (c⇩2', t⇩2) ∧ (c' = SKIP) = (c⇩2' = SKIP)) ∧
              (s = t⇩1 (⊆ sources (flow cfs) s x) ⟶
                run_flow (flow cfs) s x = t⇩2 x)"
              using B [of B⇩1 C B⇩1' D' s "[]" c s cfs c'
               "run_flow (flow cfs) s"] and N and T by force
            {
              fix x
              assume W: "s = t⇩1 (⊆ sources_aux (⟨bvars b⟩ # flow cfs) s x)"
              moreover have "sources_aux (flow cfs) s x ⊆
                sources_aux (⟨bvars b⟩ # (flow cfs)) s x"
                by (rule sources_aux_observe_tl)
              ultimately have "(c, t⇩1) →* (c⇩2', t⇩2)"
                using V by blast
              hence "(c;; WHILE b DO c, t⇩1) →* (c⇩2';; WHILE b DO c, t⇩2)"
                by (rule star_seq2)
              moreover have "s = t⇩1 (⊆ bvars b)"
                using Q and W by (blast dest: sources_aux_observe_hd)
              hence "bval b t⇩1"
                using S by (blast dest: bvars_bval)
              hence "(IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →
                (c;; WHILE b DO c, t⇩1)" ..
              ultimately have
               "(IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →*
                  (c⇩2';; WHILE b DO c, t⇩2) ∧ c⇩2';; WHILE b DO c ≠ SKIP"
                by (blast intro: star_trans)
            }
            moreover {
              fix x
              assume "s = t⇩1 (⊆ sources (⟨bvars b⟩ # flow cfs) s x)"
              moreover have "sources (flow cfs) s x ⊆
                sources (⟨bvars b⟩ # (flow cfs)) s x"
                by (rule sources_observe_tl)
              ultimately have "run_flow (flow cfs) s x = t⇩2 x"
                using V by blast
            }
            ultimately have "∃c⇩2' t⇩2. ∀x.
              (s = t⇩1 (⊆ sources_aux (⟨bvars b⟩ # flow cfs) s x) ⟶
                (IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →* (c⇩2', t⇩2) ∧
                  c⇩2' ≠ SKIP) ∧
              (s = t⇩1 (⊆ sources (⟨bvars b⟩ # flow cfs) s x) ⟶
                run_flow (flow cfs) s x = t⇩2 x)"
              by blast
          }
          moreover {
            fix s' cfs cfs'
            assume
              V: "length cfs' < length cfs⇩2 - Suc 0" and
              W: "(c, s) →*{cfs} (SKIP, s')" and
              X: "(WHILE b DO c, s') →*{cfs'}
                (c⇩2, run_flow (flow cfs') (run_flow (flow cfs) s))"
            then obtain c⇩2' and t⇩2 where "∀x.
              (s = t⇩1 (⊆ sources_aux (flow cfs) s x) ⟶
                (c, t⇩1) →* (c⇩2', t⇩2) ∧ (SKIP = SKIP) = (c⇩2' = SKIP)) ∧
              (s = t⇩1 (⊆ sources (flow cfs) s x) ⟶ s' x = t⇩2 x)"
              using B [of B⇩1 C B⇩1' D' s "[]" c s cfs SKIP s']
               and N and T by force
            moreover have Y: "s' = run_flow (flow cfs) s"
              using W by (rule small_stepsl_run_flow)
            ultimately have Z: "∀x.
              (s = t⇩1 (⊆ sources_aux (flow cfs) s x) ⟶
                (c, t⇩1) →* (SKIP, t⇩2)) ∧
              (s = t⇩1 (⊆ sources (flow cfs) s x) ⟶
                run_flow (flow cfs) s x = t⇩2 x)"
              by blast
            assume "s⇩2 = run_flow (flow cfs') (run_flow (flow cfs) s)"
            moreover have "(c, s) ⇒ s'"
              using W by (auto dest: small_stepsl_steps simp: big_iff_small)
            hence "s' ∈ Univ C (⊆ state ∩ Y)"
              using M and S by blast
            ultimately obtain c⇩3' and t⇩3 where AA: "∀x.
              (run_flow (flow cfs) s = t⇩2
                (⊆ sources_aux (flow cfs') (run_flow (flow cfs) s) x) ⟶
                  (WHILE b DO c, t⇩2) →* (c⇩3', t⇩3) ∧
                  (c⇩2 = SKIP) = (c⇩3' = SKIP)) ∧
              (run_flow (flow cfs) s = t⇩2
                (⊆ sources (flow cfs') (run_flow (flow cfs) s) x) ⟶
                  run_flow (flow cfs') (run_flow (flow cfs) s) x = t⇩3 x)"
              using K [of cfs' "[]" cfs' s' "WHILE b DO c" s']
               and V and X and Y by force
            {
              fix x
              assume AB: "s = t⇩1
                (⊆ sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x)"
              moreover have "sources_aux (flow cfs) s x ⊆
                sources_aux (flow cfs @ flow cfs') s x"
                by (rule sources_aux_append)
              moreover have AC: "sources_aux (flow cfs @ flow cfs') s x ⊆
                sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                by (rule sources_aux_observe_tl)
              ultimately have "(c, t⇩1) →* (SKIP, t⇩2)"
                using Z by blast
              hence "(c;; WHILE b DO c, t⇩1) →* (SKIP;; WHILE b DO c, t⇩2)"
                by (rule star_seq2)
              moreover have "s = t⇩1 (⊆ bvars b)"
                using Q and AB by (blast dest: sources_aux_observe_hd)
              hence "bval b t⇩1"
                using S by (blast dest: bvars_bval)
              hence "(IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →
                (c;; WHILE b DO c, t⇩1)" ..
              ultimately have "(IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →*
                (WHILE b DO c, t⇩2)"
                by (blast intro: star_trans)
              moreover have "run_flow (flow cfs) s = t⇩2
                (⊆ sources_aux (flow cfs') (run_flow (flow cfs) s) x)"
              proof
                fix y
                assume "y ∈ sources_aux (flow cfs')
                  (run_flow (flow cfs) s) x"
                hence "sources (flow cfs) s y ⊆
                  sources_aux (flow cfs @ flow cfs') s x"
                  by (rule sources_aux_member)
                hence "sources (flow cfs) s y ⊆
                  sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                  using AC by simp
                thus "run_flow (flow cfs) s y = t⇩2 y"
                  using Z and AB by blast
              qed
              hence "(WHILE b DO c, t⇩2) →* (c⇩3', t⇩3) ∧
                (c⇩2 = SKIP) = (c⇩3' = SKIP)"
                using AA by simp
              ultimately have
               "(IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →*
                  (c⇩3', t⇩3) ∧ (c⇩2 = SKIP) = (c⇩3' = SKIP)"
                by (blast intro: star_trans)
            }
            moreover {
              fix x
              assume AB: "s = t⇩1
                (⊆ sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x)"
              have "run_flow (flow cfs) s = t⇩2
                (⊆ sources (flow cfs') (run_flow (flow cfs) s) x)"
              proof
                fix y
                assume "y ∈ sources (flow cfs')
                  (run_flow (flow cfs) s) x"
                hence "sources (flow cfs) s y ⊆
                  sources (flow cfs @ flow cfs') s x"
                  by (rule sources_member)
                moreover have "sources (flow cfs @ flow cfs') s x ⊆
                  sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                  by (rule sources_observe_tl)
                ultimately have "sources (flow cfs) s y ⊆
                  sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x"
                  by simp
                thus "run_flow (flow cfs) s y = t⇩2 y"
                  using Z and AB by blast
              qed
              hence "run_flow (flow cfs') (run_flow (flow cfs) s) x = t⇩3 x"
                using AA by simp
            }
            ultimately have "∃c⇩3' t⇩3. ∀x.
              (s = t⇩1
                (⊆ sources_aux (⟨bvars b⟩ # flow cfs @ flow cfs') s x) ⟶
                  (IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →* (c⇩3', t⇩3) ∧
                  (c⇩2 = SKIP) = (c⇩3' = SKIP)) ∧
              (s = t⇩1
                (⊆ sources (⟨bvars b⟩ # flow cfs @ flow cfs') s x) ⟶
                  run_flow (flow cfs') (run_flow (flow cfs) s) x = t⇩3 x)"
              by auto
          }
          ultimately show ?thesis
            using R by (auto simp: run_flow_append)
        next
          assume
            S: "¬ bval b s" and
            T: "flow cfs⇩2 = ⟨bvars b⟩ # flow (tl cfs⇩2)"
          assume "(SKIP, s) →*{tl cfs⇩2} (c⇩2, s⇩2)"
          hence U: "(c⇩2, s⇩2) = (SKIP, s) ∧ flow (tl cfs⇩2) = []"
            by (rule small_stepsl_skip)
          show ?thesis
          proof (rule exI [of _ SKIP], rule exI [of _ t⇩1])
            {
              fix x
              assume "s = t⇩1 (⊆ sources_aux [⟨bvars b⟩] s x)"
              hence "s = t⇩1 (⊆ bvars b)"
                using Q by (blast dest: sources_aux_observe_hd)
              hence "¬ bval b t⇩1"
                using S by (blast dest: bvars_bval)
              hence "(IF b THEN c;; WHILE b DO c ELSE SKIP, t⇩1) →
                (SKIP, t⇩1)" ..
            }
            moreover {
              fix x
              assume "s = t⇩1 (⊆ sources [⟨bvars b⟩] s x)"
              hence "s x = t⇩1 x"
                by (subst (asm) append_Nil [symmetric],
                 simp only: sources.simps, auto)
            }
            ultimately show "∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
                (c⇩1, t⇩1) →* (SKIP, t⇩1) ∧ (c⇩2 = SKIP) = (SKIP = SKIP)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩1 x)"
              using R and T and U by auto
          qed
        qed
      next
        assume R: "bval b s"
        with F and O and P have S: "s ∈ Univ B⇩1' (⊆ state ∩ Y)"
          by (drule_tac btyping2_approx [where s = s], auto)
        assume "(c;; WHILE b DO c, s) →*{tl2 cfs⇩1} (c⇩1, s⇩1)"
        hence
         "(∃c' cfs'. c⇩1 = c';; WHILE b DO c ∧
            (c, s) →*{cfs'} (c', s⇩1) ∧
            flow (tl2 cfs⇩1) = flow cfs') ∨
          (∃s' cfs' cfs''. length cfs'' < length (tl2 cfs⇩1) ∧
            (c, s) →*{cfs'} (SKIP, s') ∧
            (WHILE b DO c, s') →*{cfs''} (c⇩1, s⇩1) ∧
            flow (tl2 cfs⇩1) = flow cfs' @ flow cfs'')"
          by (rule small_stepsl_seq)
        moreover {
          fix c' cfs
          assume
            T: "(c, s) →*{cfs} (c', s⇩1)" and
            U: "c⇩1 = c';; WHILE b DO c"
          hence V: "(c';; WHILE b DO c, s⇩1) →*{cfs⇩2} (c⇩2, s⇩2)"
            using J by simp
          hence W: "s⇩2 = run_flow (flow cfs⇩2) s⇩1"
            by (rule small_stepsl_run_flow)
          have
           "(∃c'' cfs'. c⇩2 = c'';; WHILE b DO c ∧
              (c', s⇩1) →*{cfs'} (c'', s⇩2) ∧
              flow cfs⇩2 = flow cfs') ∨
            (∃s' cfs' cfs''. length cfs'' < length cfs⇩2 ∧
              (c', s⇩1) →*{cfs'} (SKIP, s') ∧
              (WHILE b DO c, s') →*{cfs''} (c⇩2, s⇩2) ∧
              flow cfs⇩2 = flow cfs' @ flow cfs'')"
            using V by (rule small_stepsl_seq)
          moreover {
            fix c'' cfs'
            assume "(c', s⇩1) →*{cfs'} (c'', s⇩2)"
            then obtain c⇩2' and t⇩2 where X: "∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs') s⇩1 x) ⟶
                (c', t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs') s⇩1 x) ⟶
                run_flow (flow cfs⇩2) s⇩1 x = t⇩2 x)"
              using B [of B⇩1 C B⇩1' D' s cfs c' s⇩1 cfs' c''
               "run_flow (flow cfs⇩2) s⇩1"] and N and S and T and W by force
            assume
              Y: "c⇩2 = c'';; WHILE b DO c" and
              Z: "flow cfs⇩2 = flow cfs'"
            have ?thesis
            proof (rule exI [of _ "c⇩2';; WHILE b DO c"], rule exI [of _ t⇩2])
              from U and W and X and Y and Z show "∀x.
                (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
                  (c⇩1, t⇩1) →* (c⇩2';; WHILE b DO c, t⇩2) ∧
                    (c⇩2 = SKIP) = (c⇩2';; WHILE b DO c = SKIP)) ∧
                (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)"
                by (auto intro: star_seq2)
            qed
          }
          moreover {
            fix s' cfs' cfs''
            assume
              X: "length cfs'' < length cfs⇩2" and
              Y: "(c', s⇩1) →*{cfs'} (SKIP, s')" and
              Z: "(WHILE b DO c, s') →*{cfs''} (c⇩2, s⇩2)"
            then obtain c⇩2' and t⇩2 where "∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs') s⇩1 x) ⟶
                (c', t⇩1) →* (c⇩2', t⇩2) ∧ (SKIP = SKIP) = (c⇩2' = SKIP)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs') s⇩1 x) ⟶ s' x = t⇩2 x)"
              using B [of B⇩1 C B⇩1' D' s cfs c' s⇩1 cfs' SKIP s']
               and N and S and T by force
            moreover have AA: "s' = run_flow (flow cfs') s⇩1"
              using Y by (rule small_stepsl_run_flow)
            ultimately have AB: "∀x.
              (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs') s⇩1 x) ⟶
                (c', t⇩1) →* (SKIP, t⇩2)) ∧
              (s⇩1 = t⇩1 (⊆ sources (flow cfs') s⇩1 x) ⟶
                run_flow (flow cfs') s⇩1 x = t⇩2 x)"
              by blast
            have AC: "s⇩2 = run_flow (flow cfs'') s'"
              using Z by (rule small_stepsl_run_flow)
            moreover have "(c, s) →*{cfs @ cfs'} (SKIP, s')"
              using T and Y by (simp add: small_stepsl_append)
            hence "(c, s) ⇒ s'"
              by (auto dest: small_stepsl_steps simp: big_iff_small)
            hence "s' ∈ Univ C (⊆ state ∩ Y)"
              using M and R by blast
            ultimately obtain c⇩2' and t⇩3 where AD: "∀x.
              (run_flow (flow cfs') s⇩1 = t⇩2
                (⊆ sources_aux (flow cfs'') (run_flow (flow cfs') s⇩1) x) ⟶
                  (WHILE b DO c, t⇩2) →* (c⇩2', t⇩3) ∧
                  (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
              (run_flow (flow cfs') s⇩1 = t⇩2
                (⊆ sources (flow cfs'') (run_flow (flow cfs') s⇩1) x) ⟶
                  run_flow (flow cfs'') (run_flow (flow cfs') s⇩1) x = t⇩3 x)"
              using K [of cfs'' "[]" cfs'' s' "WHILE b DO c" s']
               and X and Z and AA by force
            moreover assume "flow cfs⇩2 = flow cfs' @ flow cfs''"
            moreover {
              fix x
              assume AE: "s⇩1 = t⇩1
                (⊆ sources_aux (flow cfs' @ flow cfs'') s⇩1 x)"
              moreover have "sources_aux (flow cfs') s⇩1 x ⊆
                sources_aux (flow cfs' @ flow cfs'') s⇩1 x"
                by (rule sources_aux_append)
              ultimately have "(c', t⇩1) →* (SKIP, t⇩2)"
                using AB by blast
              hence "(c';; WHILE b DO c, t⇩1) →* (SKIP;; WHILE b DO c, t⇩2)"
                by (rule star_seq2)
              hence "(c';; WHILE b DO c, t⇩1) →* (WHILE b DO c, t⇩2)"
                by (blast intro: star_trans)
              moreover have "run_flow (flow cfs') s⇩1 = t⇩2
                (⊆ sources_aux (flow cfs'') (run_flow (flow cfs') s⇩1) x)"
              proof
                fix y
                assume "y ∈ sources_aux (flow cfs'')
                  (run_flow (flow cfs') s⇩1) x"
                hence "sources (flow cfs') s⇩1 y ⊆
                  sources_aux (flow cfs' @ flow cfs'') s⇩1 x"
                  by (rule sources_aux_member)
                thus "run_flow (flow cfs') s⇩1 y = t⇩2 y"
                  using AB and AE by blast
              qed
              hence "(WHILE b DO c, t⇩2) →* (c⇩2', t⇩3) ∧
                (c⇩2 = SKIP) = (c⇩2' = SKIP)"
                using AD by simp
              ultimately have "(c';; WHILE b DO c, t⇩1) →* (c⇩2', t⇩3) ∧
                (c⇩2 = SKIP) = (c⇩2' = SKIP)"
                by (blast intro: star_trans)
            }
            moreover {
              fix x
              assume AE: "s⇩1 = t⇩1
                (⊆ sources (flow cfs' @ flow cfs'') s⇩1 x)"
              have "run_flow (flow cfs') s⇩1 = t⇩2
                (⊆ sources (flow cfs'') (run_flow (flow cfs') s⇩1) x)"
              proof
                fix y
                assume "y ∈ sources (flow cfs'')
                  (run_flow (flow cfs') s⇩1) x"
                hence "sources (flow cfs') s⇩1 y ⊆
                  sources (flow cfs' @ flow cfs'') s⇩1 x"
                  by (rule sources_member)
                thus "run_flow (flow cfs') s⇩1 y = t⇩2 y"
                  using AB and AE by blast
              qed
              hence "run_flow (flow cfs'')
                (run_flow (flow cfs') s⇩1) x = t⇩3 x"
                using AD by simp
            }
            ultimately have ?thesis
              by (metis U AA AC)
          }
          ultimately have ?thesis
            by blast
        }
        moreover {
          fix s' cfs cfs'
          assume
           "length cfs' < length (tl2 cfs⇩1)" and
           "(c, s) →*{cfs} (SKIP, s')" and
           "(WHILE b DO c, s') →*{cfs'} (c⇩1, s⇩1)"
          moreover from this have "(c, s) ⇒ s'"
            by (auto dest: small_stepsl_steps simp: big_iff_small)
          hence "s' ∈ Univ C (⊆ state ∩ Y)"
            using M and R by blast
          ultimately have ?thesis
            using K [of "cfs' @ cfs⇩2" cfs' cfs⇩2 s' c⇩1 s⇩1] and J by force
        }
        ultimately show ?thesis
          by blast
      next
        assume "(SKIP, s) →*{tl2 cfs⇩1} (c⇩1, s⇩1)"
        hence "(c⇩1, s⇩1) = (SKIP, s)"
          by (blast dest: small_stepsl_skip)
        moreover from this have "(c⇩2, s⇩2) = (SKIP, s) ∧ flow cfs⇩2 = []"
          using J by (blast dest: small_stepsl_skip)
        ultimately show ?thesis
          by auto
      qed
    qed
  }
  ultimately show
   "(∀t⇩1. ∃c⇩2' t⇩2. ∀x.
      (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
        (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
      (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
    (∀x. (∃(B, Y) ∈ U. ∃s ∈ B. ∃y ∈ Y. ¬ s: dom y ↝ dom x) ⟶
      no_upd (flow cfs⇩2) x)"
    using L by auto
qed

lemma ctyping2_correct_aux:
 "⟦(U, v) ⊨ c (⊆ A, X) = Some (B, Y); s ∈ Univ A (⊆ state ∩ X);
    (c, s) →*{cfs⇩1} (c⇩1, s⇩1); (c⇩1, s⇩1) →*{cfs⇩2} (c⇩2, s⇩2)⟧ ⟹
  ok_flow_aux U c⇩1 c⇩2 s⇩1 s⇩2 (flow cfs⇩2)"
proof (induction "(U, v)" c A X arbitrary: B Y U v s c⇩1 c⇩2 s⇩1 s⇩2 cfs⇩1 cfs⇩2
 rule: ctyping2.induct)
  fix A X C Z U v c⇩1 c⇩2 c' c'' s s⇩1 s⇩2 cfs⇩1 cfs⇩2
  show
   "⟦⋀B Y s c' c'' s⇩1 s⇩2 cfs⇩1 cfs⇩2.
      (U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ⟹
      s ∈ Univ A (⊆ state ∩ X) ⟹
      (c⇩1, s) →*{cfs⇩1} (c', s⇩1) ⟹
      (c', s⇩1) →*{cfs⇩2} (c'', s⇩2) ⟹
      (∀t⇩1. ∃c⇩2' t⇩2. ∀x.
        (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
          (c', t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
        (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
      (∀x. (∃(B, W) ∈ U. ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
        no_upd (flow cfs⇩2) x);
    ⋀p B Y C Z s c' c'' s⇩1 s⇩2 cfs⇩1 cfs⇩2.
      (U, v) ⊨ c⇩1 (⊆ A, X) = Some p ⟹
      (B, Y) = p ⟹
      (U, v) ⊨ c⇩2 (⊆ B, Y) = Some (C, Z) ⟹
      s ∈ Univ B (⊆ state ∩ Y) ⟹
      (c⇩2, s) →*{cfs⇩1} (c', s⇩1) ⟹
      (c', s⇩1) →*{cfs⇩2} (c'', s⇩2) ⟹
      (∀t⇩1. ∃c⇩2'' t⇩2. ∀x.
        (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
          (c', t⇩1) →* (c⇩2'', t⇩2) ∧ (c'' = SKIP) = (c⇩2'' = SKIP)) ∧
        (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
      (∀x. (∃(B, W) ∈ U. ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
        no_upd (flow cfs⇩2) x);
    (U, v) ⊨ c⇩1;; c⇩2 (⊆ A, X) = Some (C, Z);
    s ∈ Univ A (⊆ state ∩ X);
    (c⇩1;; c⇩2, s) →*{cfs⇩1} (c', s⇩1);
    (c', s⇩1) →*{cfs⇩2} (c'', s⇩2)⟧ ⟹
      (∀t⇩1. ∃c⇩2' t⇩2. ∀x.
        (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
          (c', t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
        (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
      (∀x. (∃(B, W) ∈ U. ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
        no_upd (flow cfs⇩2) x)"
    by (auto del: conjI split: option.split_asm,
     rule ctyping2_correct_aux_seq)
next
  fix A X C Y U v b c⇩1 c⇩2 c' c'' s s⇩1 s⇩2 cfs⇩1 cfs⇩2
  show
   "⟦⋀U' p B⇩1 B⇩2 C Y s c' c'' s⇩1 s⇩2 cfs⇩1 cfs⇩2.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B⇩1, B⇩2) = p ⟹
      (U', v) ⊨ c⇩1 (⊆ B⇩1, X) = Some (C, Y) ⟹
      s ∈ Univ B⇩1 (⊆ state ∩ X) ⟹
      (c⇩1, s) →*{cfs⇩1} (c', s⇩1) ⟹
      (c', s⇩1) →*{cfs⇩2} (c'', s⇩2) ⟹
      (∀t⇩1. ∃c⇩2' t⇩2. ∀x.
        (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
          (c', t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
        (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
      (∀x. (∃(B, W) ∈ U'. ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
        no_upd (flow cfs⇩2) x);
    ⋀U' p B⇩1 B⇩2 C Y s c' c'' s⇩1 s⇩2 cfs⇩1 cfs⇩2.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B⇩1, B⇩2) = p ⟹
      (U', v) ⊨ c⇩2 (⊆ B⇩2, X) = Some (C, Y) ⟹
      s ∈ Univ B⇩2 (⊆ state ∩ X) ⟹
      (c⇩2, s) →*{cfs⇩1} (c', s⇩1) ⟹
      (c', s⇩1) →*{cfs⇩2} (c'', s⇩2) ⟹
      (∀t⇩1. ∃c⇩2'' t⇩2. ∀x.
        (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
          (c', t⇩1) →* (c⇩2'', t⇩2) ∧ (c'' = SKIP) = (c⇩2'' = SKIP)) ∧
        (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
      (∀x. (∃(B, W) ∈ U'. ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
        no_upd (flow cfs⇩2) x);
    (U, v) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X) = Some (C, Y);
    s ∈ Univ A (⊆ state ∩ X);
    (IF b THEN c⇩1 ELSE c⇩2, s) →*{cfs⇩1} (c', s⇩1);
    (c', s⇩1) →*{cfs⇩2} (c'', s⇩2)⟧ ⟹
      (∀t⇩1. ∃c⇩2' t⇩2. ∀x.
        (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
          (c', t⇩1) →* (c⇩2', t⇩2) ∧ (c'' = SKIP) = (c⇩2' = SKIP)) ∧
        (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
      (∀x. (∃(B, W) ∈ U. ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
        no_upd (flow cfs⇩2) x)"
    by (auto del: conjI split: option.split_asm prod.split_asm,
     rule ctyping2_correct_aux_if)
next
  fix A X B Y U v b c c⇩1 c⇩2 s s⇩1 s⇩2 cfs⇩1 cfs⇩2
  show
   "⟦⋀B⇩1 B⇩2 C Y B⇩1' B⇩2' D Z s c⇩1 c⇩2 s⇩1 s⇩2 cfs⇩1 cfs⇩2.
      (B⇩1, B⇩2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B⇩1, X) ⟹
      (B⇩1', B⇩2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: dom ` W ↝ UNIV ⟹
      ({}, False) ⊨ c (⊆ B⇩1, X) = Some (D, Z) ⟹
      s ∈ Univ B⇩1 (⊆ state ∩ X) ⟹
      (c, s) →*{cfs⇩1} (c⇩1, s⇩1) ⟹
      (c⇩1, s⇩1) →*{cfs⇩2} (c⇩2, s⇩2) ⟹
      (∀t⇩1. ∃c⇩2' t⇩2. ∀B⇩1.
        (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 B⇩1) ⟶
          (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
        (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 B⇩1) ⟶ s⇩2 B⇩1 = t⇩2 B⇩1)) ∧
      (∀x. (∃(B, W) ∈ {}. ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
        no_upd (flow cfs⇩2) x);
    ⋀B⇩1 B⇩2 C Y B⇩1' B⇩2' D' Z' s c⇩1 c⇩2 s⇩1 s⇩2 cfs⇩1 cfs⇩2.
      (B⇩1, B⇩2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B⇩1, X) ⟹
      (B⇩1', B⇩2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: dom ` W ↝ UNIV ⟹
      ({}, False) ⊨ c (⊆ B⇩1', Y) = Some (D', Z') ⟹
      s ∈ Univ B⇩1' (⊆ state ∩ Y) ⟹
      (c, s) →*{cfs⇩1} (c⇩1, s⇩1) ⟹
      (c⇩1, s⇩1) →*{cfs⇩2} (c⇩2, s⇩2) ⟹
      (∀t⇩1. ∃c⇩2' t⇩2. ∀B⇩1.
        (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 B⇩1) ⟶
          (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
        (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 B⇩1) ⟶ s⇩2 B⇩1 = t⇩2 B⇩1)) ∧
      (∀x. (∃(B, W) ∈ {}. ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
        no_upd (flow cfs⇩2) x);
    (U, v) ⊨ WHILE b DO c (⊆ A, X) = Some (B, Y);
    s ∈ Univ A (⊆ state ∩ X);
    (WHILE b DO c, s) →*{cfs⇩1} (c⇩1, s⇩1);
    (c⇩1, s⇩1) →*{cfs⇩2} (c⇩2, s⇩2)⟧ ⟹
      (∀t⇩1. ∃c⇩2' t⇩2. ∀x.
        (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs⇩2) s⇩1 x) ⟶
          (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
        (s⇩1 = t⇩1 (⊆ sources (flow cfs⇩2) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)) ∧
      (∀x. (∃(B, W) ∈ U. ∃s ∈ B. ∃y ∈ W. ¬ s: dom y ↝ dom x) ⟶
        no_upd (flow cfs⇩2) x)"
    by (auto del: conjI split: option.split_asm prod.split_asm,
     rule ctyping2_correct_aux_while, assumption+, blast)
qed (auto del: conjI split: prod.split_asm)


theorem ctyping2_correct:
  assumes A: "(U, v) ⊨ c (⊆ A, X) = Some (B, Y)"
  shows "correct c A X"
proof -
  {
    fix c⇩1 c⇩2 s⇩1 s⇩2 cfs t⇩1
    assume "ok_flow_aux U c⇩1 c⇩2 s⇩1 s⇩2 (flow cfs)"
    then obtain c⇩2' and t⇩2 where A: "∀x.
      (s⇩1 = t⇩1 (⊆ sources_aux (flow cfs) s⇩1 x) ⟶
        (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP)) ∧
      (s⇩1 = t⇩1 (⊆ sources (flow cfs) s⇩1 x) ⟶ s⇩2 x = t⇩2 x)"
      by blast
    have "∃c⇩2' t⇩2. ∀x. s⇩1 = t⇩1 (⊆ sources (flow cfs) s⇩1 x) ⟶
      (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP) ∧ s⇩2 x = t⇩2 x"
    proof (rule exI [of _ c⇩2'], rule exI [of _ t⇩2])
      have "∀x. s⇩1 = t⇩1 (⊆ sources (flow cfs) s⇩1 x) ⟶
        s⇩1 = t⇩1 (⊆ sources_aux (flow cfs) s⇩1 x)"
      proof (rule allI, rule impI)
        fix x
        assume "s⇩1 = t⇩1 (⊆ sources (flow cfs) s⇩1 x)"
        moreover have "sources_aux (flow cfs) s⇩1 x ⊆
          sources (flow cfs) s⇩1 x"
          by (rule sources_aux_sources)
        ultimately show "s⇩1 = t⇩1 (⊆ sources_aux (flow cfs) s⇩1 x)"
          by blast
      qed
      with A show "∀x. s⇩1 = t⇩1 (⊆ sources (flow cfs) s⇩1 x) ⟶
        (c⇩1, t⇩1) →* (c⇩2', t⇩2) ∧ (c⇩2 = SKIP) = (c⇩2' = SKIP) ∧ s⇩2 x = t⇩2 x"
        by auto
    qed
  }
  with A show ?thesis
    by (clarsimp dest!: small_steps_stepsl simp: correct_def,
     drule_tac ctyping2_correct_aux, auto)
qed

end

end