Theory Correctness_Theorem

(*  Title:       Extension of Stateful Intransitive Noninterference with Inputs, Outputs, and Nondeterminism 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: main theorem"

theory Correctness_Theorem
  imports Correctness_Lemmas
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 lemma @{text ctyping2_approx} proven in a previous section.
›


subsection "Local context proofs"

context noninterf
begin


lemma ctyping2_correct_aux_skip [elim!]:
 "⟦(SKIP, s, f, vs0, ws0) →*{cfs1} (c1, s1, f, vs1, ws1);
    (c1, s1, f, vs1, ws1) →*{cfs2} (c2, s2, f, vs2, ws2)⟧ ⟹
  ok_flow_aux U c1 c2 s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)"
by (fastforce dest: small_stepsl_skip)

lemma ctyping2_correct_aux_assign:
  assumes
    A: "(U, v) ⊨ x ::= a (⊆ A, X) = Some (C, Y)" and
    B: "s ∈ Univ A (⊆ state ∩ X)" and
    C: "(x ::= a, s, f, vs0, ws0) →*{cfs1} (c1, s1, f, vs1, ws1)" and
    D: "(c1, s1, f, vs1, ws1) →*{cfs2} (c2, s2, f, vs2, ws2)"
  shows "ok_flow_aux U c1 c2 s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)"
proof -
  from A have E: "∀(B, Y) ∈ insert (Univ? A X, avars a) U. B: Y ↝ {x}"
    by (simp split: if_split_asm)
  have
   "(c1, s1, f, vs1, ws1) = (x ::= a, s, f, vs0, ws0) ∨
    (c1, s1, f, vs1, ws1) = (SKIP, s(x := aval a s), f, vs0, ws0)"
    (is "?P ∨ ?Q")
    using C by (blast dest: small_stepsl_assign)
  thus ?thesis
  proof
    assume ?P
    hence "(x ::= a, s, f, vs0, ws0) →*{cfs2} (c2, s2, f, vs2, ws2)"
      using D by simp
    hence
     "(c2, s2, f, vs2, ws2) = (x ::= a, s, f, vs0, ws0) ∧
        flow cfs2 = [] ∨
      (c2, s2, f, vs2, ws2) = (SKIP, s(x := aval a s), f, vs0, ws0) ∧
        flow cfs2 = [x ::= a]"
      (is "?P' ∨ _")
      by (rule small_stepsl_assign)
    thus ?thesis
    proof (rule disjE, erule_tac [2] conjE)
      assume ?P'
      with `?P` show ?thesis
        by fastforce
    next
      assume
        F: "(c2, s2, f, vs2, ws2) = (SKIP, s(x := aval a s), f, vs0, ws0)" and
        G: "flow cfs2 = [x ::= a]"
          (is "?cs = _")
      show ?thesis
      proof (rule conjI, clarify)
        fix t1 f' vs1' ws1'
        let ?t2 = "t1(x := aval a t1)"
        show "∃c2' t2 vs2' ws2'.
          ok_flow_aux_1 c1 c2 c2' s1 t1 t2 f f'
            vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
          ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
          ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
        proof (rule exI [of _ SKIP], rule exI [of _ ?t2],
         rule exI [of _ vs1'], rule exI [of _ ws1'])
          {
            fix S
            assume "S ⊆ {y. s = t1 (⊆ sources [x ::= a] vs0 s f y)}" and
             "x ∈ S"
            hence "s = t1 (⊆ avars a)"
              using B by (rule eq_states_assign, insert E, simp)
            hence "aval a s = aval a t1"
              by (rule avars_aval)
          }
          moreover {
            fix S y
            assume "S ⊆ {y. s = t1 (⊆ sources [x ::= a] vs0 s f y)}" and
             "y ∈ S"
            hence "s = t1 (⊆ sources [x ::= a] vs0 s f y)"
              by blast
            moreover assume "y ≠ x"
            ultimately have "s y = t1 y"
              by (subst (asm) append_Nil [symmetric],
               simp only: sources.simps, simp)
          }
          ultimately show
           "ok_flow_aux_1 c1 c2 SKIP s1 t1 ?t2 f f'
              vs1 vs1' vs2 vs1' ws1' ws1' ?cs ∧
            ok_flow_aux_2 s1 s2 t1 ?t2 f f' vs1 vs1' ?cs ∧
            ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws1' ?cs"
            using F and G and `?P` by auto
        qed
      qed (insert E G, fastforce)
    qed
  next
    assume ?Q
    moreover from this have
     "(c2, s2, f, vs2, ws2) = (SKIP, s1, f, vs1, ws1) ∧ flow cfs2 = []"
      using D by (blast intro!: small_stepsl_skip)
    ultimately show ?thesis
      by fastforce
  qed
qed

lemma ctyping2_correct_aux_input:
  assumes
    A: "(U, v) ⊨ IN x (⊆ A, X) = Some (C, Y)" and
    B: "(IN x, s, f, vs0, ws0) →*{cfs1} (c1, s1, f, vs1, ws1)" and
    C: "(c1, s1, f, vs1, ws1) →*{cfs2} (c2, s2, f, vs2, ws2)"
  shows "ok_flow_aux U c1 c2 s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)"
proof -
  from A have D: "∀(B, Y) ∈ U. B: Y ↝ {x}"
    by (simp split: if_split_asm)
  let ?n = "length [p←vs0. fst p = x]"
  have
   "(c1, s1, f, vs1, ws1) = (IN x, s, f, vs0, ws0) ∨
    (c1, s1, f, vs1, ws1) =
      (SKIP, s(x := f x ?n), f, vs0 @ [(x, f x ?n)], ws0)"
    (is "?P ∨ ?Q")
    using B by (auto dest: small_stepsl_input simp: Let_def)
  thus ?thesis
  proof
    assume ?P
    hence "(IN x, s, f, vs0, ws0) →*{cfs2} (c2, s2, f, vs2, ws2)"
      using C by simp
    hence
     "(c2, s2, f, vs2, ws2) = (IN x, s, f, vs0, ws0) ∧
        flow cfs2 = [] ∨
      (c2, s2, f, vs2, ws2) =
        (SKIP, s(x := f x ?n), f, vs0 @ [(x, f x ?n)], ws0) ∧
        flow cfs2 = [IN x]"
      (is "?P' ∨ _")
      by (auto dest: small_stepsl_input simp: Let_def)
    thus ?thesis
    proof (rule disjE, erule_tac [2] conjE)
      assume ?P'
      with `?P` show ?thesis
        by fastforce
    next
      assume
        E: "(c2, s2, f, vs2, ws2) =
          (SKIP, s(x := f x ?n), f, vs0 @ [(x, f x ?n)], ws0)" and
        F: "flow cfs2 = [IN x]"
          (is "?cs = _")
      show ?thesis
      proof (rule conjI, clarify)
        fix t1 f' vs1' ws1'
        let ?n' = "length [p←vs1' :: inputs. fst p = x]"
        let ?t2 = "t1(x := f' x ?n') :: state" and
          ?vs2' = "vs1' @ [(x, f' x ?n')]"
        show "∃c2' t2 vs2' ws2'.
          ok_flow_aux_1 c1 c2 c2' s1 t1 t2 f f'
            vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
          ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
          ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
        proof (rule exI [of _ SKIP], rule exI [of _ ?t2],
         rule exI [of _ ?vs2'], rule exI [of _ ws1'])
          {
            fix S
            assume "f = f' (⊆ vs0, vs1',
              ⋃ {tags [IN x] vs0 s f y | y. y ∈ S})"
                (is "_ = _ (⊆ _, _, ?T)")
            moreover assume "x ∈ S"
            hence "tags [IN x] vs0 s f x ⊆ ?T"
              by blast
            ultimately have "f = f' (⊆ vs0, vs1', tags [IN x] vs0 s f x)"
              by (rule eq_streams_subset)
            moreover have "tags [IN x] vs0 s f x = {(x, 0)}"
              by (subst append_Nil [symmetric],
               simp only: tags.simps, simp)
            ultimately have "f x (length [p←vs0. fst p = x]) =
              f' x (length [p←vs1'. fst p = x])"
              by (simp add: eq_streams_def)
          }
          moreover
          {
            fix S y
            assume "S ⊆ {y. s = t1 (⊆ sources [IN x] vs0 s f y)}" and
             "y ∈ S"
            hence "s = t1 (⊆ sources [IN x] vs0 s f y)"
              by blast
            moreover assume "y ≠ x"
            ultimately have "s y = t1 y"
              by (subst (asm) append_Nil [symmetric],
               simp only: sources.simps, simp)
          }
          ultimately show
           "ok_flow_aux_1 c1 c2 SKIP s1 t1 ?t2 f f'
              vs1 vs1' vs2 ?vs2' ws1' ws1' ?cs ∧
            ok_flow_aux_2 s1 s2 t1 ?t2 f f' vs1 vs1' ?cs ∧
            ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws1' ?cs"
            using E and F and `?P` by auto
        qed
      qed (insert D F, fastforce)
    qed
  next
    assume ?Q
    moreover from this have
     "(c2, s2, f, vs2, ws2) = (SKIP, s1, f, vs1, ws1) ∧ flow cfs2 = []"
      using C by (blast intro!: small_stepsl_skip)
    ultimately show ?thesis
      by fastforce
  qed
qed

lemma ctyping2_correct_aux_output:
  assumes
    A: "(U, v) ⊨ OUT x (⊆ A, X) = Some (B, Y)" and
    B: "(OUT x, s, f, vs0, ws0) →*{cfs1} (c1, s1, f, vs1, ws1)" and
    C: "(c1, s1, f, vs1, ws1) →*{cfs2} (c2, s2, f, vs2, ws2)"
  shows "ok_flow_aux U c1 c2 s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)"
proof -
  from A have D: "∀(B, Y) ∈ U. B: Y ↝ {x}"
    by (simp split: if_split_asm)
  have
   "(c1, s1, f, vs1, ws1) = (OUT x, s, f, vs0, ws0) ∨
    (c1, s1, f, vs1, ws1) = (SKIP, s, f, vs0, ws0 @ [(x, s x)])"
    (is "?P ∨ ?Q")
    using B by (blast dest: small_stepsl_output)
  thus ?thesis
  proof
    assume ?P
    hence "(OUT x, s, f, vs0, ws0) →*{cfs2} (c2, s2, f, vs2, ws2)"
      using C by simp
    hence
     "(c2, s2, f, vs2, ws2) = (OUT x, s, f, vs0, ws0) ∧
        flow cfs2 = [] ∨
      (c2, s2, f, vs2, ws2) = (SKIP, s, f, vs0, ws0 @ [(x, s x)]) ∧
        flow cfs2 = [OUT x]"
      (is "?P' ∨ _")
      by (rule small_stepsl_output)
    thus ?thesis
    proof (rule disjE, erule_tac [2] conjE)
      assume ?P'
      with `?P` show ?thesis
        by fastforce
    next
      assume
        E: "(c2, s2, f, vs2, ws2) = (SKIP, s, f, vs0, ws0 @ [(x, s x)])" and
        F: "flow cfs2 = [OUT x]"
          (is "?cs = _")
      show ?thesis
      proof (rule conjI, clarify)
        fix t1 f' vs1' ws1'
        let ?ws2' = "ws1' @ [(x, t1 x)] :: outputs"
        show "∃c2' t2 vs2' ws2'.
          ok_flow_aux_1 c1 c2 c2' s1 t1 t2 f f'
            vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
          ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
          ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
        proof (rule exI [of _ SKIP], rule exI [of _ t1],
         rule exI [of _ vs1'], rule exI [of _ ?ws2'])
          {
            fix S y
            assume "S ⊆ {y. s = t1 (⊆ sources [OUT x] vs0 s f y)}" and
             "y ∈ S"
            hence "s = t1 (⊆ sources [OUT x] vs0 s f y)"
              by blast
            hence "s y = t1 y"
              by (subst (asm) append_Nil [symmetric],
               simp only: sources.simps, simp)
          }
          moreover {
            fix S
            assume "S ⊆ {y. s = t1 (⊆ sources_out [OUT x] vs0 s f y)}" and
             "x ∈ S"
            hence "s = t1 (⊆ sources_out [OUT x] vs0 s f x)"
              by blast
            hence "s x = t1 x"
              by (subst (asm) append_Nil [symmetric],
               simp only: sources_out.simps, simp)
          }
          ultimately show
           "ok_flow_aux_1 c1 c2 SKIP s1 t1 t1 f f'
              vs1 vs1' vs2 vs1' ws1' ?ws2' ?cs ∧
            ok_flow_aux_2 s1 s2 t1 t1 f f' vs1 vs1' ?cs ∧
            ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ?ws2' ?cs"
            using E and F and `?P` by auto
        qed
      qed (insert D F, fastforce)
    qed
  next
    assume ?Q
    moreover from this have
     "(c2, s2, f, vs2, ws2) = (SKIP, s1, f, vs1, ws1) ∧ flow cfs2 = []"
      using C by (blast intro!: small_stepsl_skip)
    ultimately show ?thesis
      by fastforce
  qed
qed

lemma ctyping2_correct_aux_seq:
  assumes
    A: "(U, v) ⊨ c1;; c2 (⊆ A, X) = Some (C, Z)" and
    B: "⋀B Y c' c'' s s1 s2 vs0 vs1 vs2 ws0 ws1 ws2 cfs1 cfs2.
      (U, v) ⊨ c1 (⊆ A, X) = Some (B, Y) ⟹
      s ∈ Univ A (⊆ state ∩ X) ⟹
      (c1, s, f, vs0, ws0) →*{cfs1} (c', s1, f, vs1, ws1) ⟹
      (c', s1, f, vs1, ws1) →*{cfs2} (c'', s2, f, vs2, ws2) ⟹
        ok_flow_aux U c' c'' s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)" and
    C: "⋀p B Y C Z c' c'' s s1 s2 vs0 vs1 vs2 ws0 ws1 ws2 cfs1 cfs2.
      (U, v) ⊨ c1 (⊆ A, X) = Some p ⟹ (B, Y) = p ⟹
      (U, v) ⊨ c2 (⊆ B, Y) = Some (C, Z) ⟹
      s ∈ Univ B (⊆ state ∩ Y) ⟹
      (c2, s, f, vs0, ws0) →*{cfs1} (c', s1, f, vs1, ws1) ⟹
      (c', s1, f, vs1, ws1) →*{cfs2} (c'', s2, f, vs2, ws2) ⟹
        ok_flow_aux U c' c'' s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)" and
    D: "s ∈ Univ A (⊆ state ∩ X)" and
    E: "(c1;; c2, s, f, vs0, ws0) →*{cfs1} (c', s1, f, vs1, ws1)" and
    F: "(c', s1, f, vs1, ws1) →*{cfs2} (c'', s2, f, vs2, ws2)"
  shows "ok_flow_aux U c' c'' s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)"
proof -
  from A obtain B and Y where
    G: "(U, v) ⊨ c1 (⊆ A, X) = Some (B, Y)" and
    H: "(U, v) ⊨ c2 (⊆ B, Y) = Some (C, Z)"
    by (auto split: option.split_asm)
  have
   "(∃c cfs. c' = c;; c2 ∧
      (c1, s, f, vs0, ws0) →*{cfs} (c, s1, f, vs1, ws1)) ∨
    (∃s' p cfs cfs'.
      (c1, s, f, vs0, ws0) →*{cfs} (SKIP, s', p) ∧
      (c2, s', p) →*{cfs'} (c', s1, f, vs1, ws1))"
    using E by (fastforce dest: small_stepsl_seq)
  thus ?thesis
  proof (rule disjE, (erule_tac exE)+, (erule_tac [2] exE)+,
   erule_tac [!] conjE)
    fix c1' cfs
    assume
      I: "c' = c1';; c2" and
      J: "(c1, s, f, vs0, ws0) →*{cfs} (c1', s1, f, vs1, ws1)"
    hence "(c1';; c2, s1, f, vs1, ws1) →*{cfs2} (c'', s2, f, vs2, ws2)"
      using F by simp
    hence
     "(∃d cfs'. c'' = d;; c2 ∧
        (c1', s1, f, vs1, ws1) →*{cfs'} (d, s2, f, vs2, ws2) ∧
        flow cfs2 = flow cfs') ∨
      (∃p cfs' cfs''.
        (c1', s1, f, vs1, ws1) →*{cfs'} (SKIP, p) ∧
        (c2, p) →*{cfs''} (c'', s2, f, vs2, ws2) ∧
        flow cfs2 = 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 c1'' cfs'
      assume
        K: "c'' = c1'';; c2" and
        L: "(c1', s1, f, vs1, ws1) →*{cfs'} (c1'', s2, f, vs2, ws2)" and
        M: "flow cfs2 = flow cfs'"
          (is "?cs = ?cs'")
      have N: "ok_flow_aux U c1' c1'' s1 s2 f vs1 vs2 ws1 ws2 ?cs'"
        using B [OF G D J L] .
      show ?thesis
      proof (rule conjI, clarify)
        fix t1 f' vs1' ws1'
        obtain c2' and t2 and vs2' and ws2' where
         "ok_flow_aux_1 c1' c1'' c2' s1 t1 t2 f f'
            vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
          ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
          ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
          (is "?P1 ∧ ?P2 ∧ ?P3")
          using M and N by fastforce
        hence ?P1 and ?P2 and ?P3 by auto
        show "∃c2' t2 vs2' ws2'.
          ok_flow_aux_1 c' c'' c2' s1 t1 t2 f f'
            vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
          ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
          ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
        proof (rule exI [of _ "c2';; c2"], rule exI [of _ t2],
         rule exI [of _ vs2'], rule exI [of _ ws2'])
          {
            fix S
            assume "S ≠ {}" and
             "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs vs1 s1 f x)}" and
             "f = f' (⊆ vs1, vs1', ⋃ {tags_aux ?cs vs1 s1 f x | x. x ∈ S})"
            hence
             "(c', t1, f', vs1', ws1') →* (c2';; c2, t2, f', vs2', ws2') ∧
              map fst [p←drop (length vs1) vs2. fst p ∈ S] =
                map fst [p←drop (length vs1') vs2'. fst p ∈ S]"
              using I and `?P1` by (blast intro: star_seq2)
          }
          thus
           "ok_flow_aux_1 c' c'' (c2';; c2) s1 t1 t2 f f'
              vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
            ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
            ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
            using K and `?P2` and `?P3` by simp
        qed
      qed (simp add: M N)
    next
      fix p cfs' cfs''
      assume "(c1', s1, f, vs1, ws1) →*{cfs'} (SKIP, p)"
      moreover from this obtain s1' and vs and ws where
        K: "p = (s1', f, vs, ws)"
        by (blast dest: small_stepsl_stream)
      ultimately have
        L: "(c1', s1, f, vs1, ws1) →*{cfs'} (SKIP, s1', f, vs, ws)"
        by simp
      assume "(c2, p) →*{cfs''} (c'', s2, f, vs2, ws2)"
      with K have
        M: "(c2, s1', f, vs, ws) →*{cfs''} (c'', s2, f, vs2, ws2)"
        by simp
      assume N: "flow cfs2 = flow cfs' @ flow cfs''"
        (is "(?cs :: flow) = ?cs' @ ?cs''")
      have O: "ok_flow_aux U c1' SKIP s1 s1' f vs1 vs ws1 ws ?cs'"
        using B [OF G D J L] .
      have "(c1, s, f, vs0, ws0) →*{cfs @ cfs'} (SKIP, s1', f, vs, ws)"
        using J and L by (simp add: small_stepsl_append)
      hence "(c1, s, f, vs0, ws0) ⇒ (s1', f, vs, ws)"
        by (auto dest: small_stepsl_steps simp: big_iff_small)
      hence P: "s1' ∈ Univ B (⊆ state ∩ Y)"
        using G and D by (rule ctyping2_approx)
      have Q: "ok_flow_aux U c2 c'' s1' s2 f vs vs2 ws ws2 ?cs''"
        using C [OF G _ H P _ M, of vs ws "[]"] by simp
      show ?thesis
      proof (rule conjI, clarify)
        fix t1 f' vs1' ws1'
        obtain c1'' and t1' and vs1'' and ws1'' where
         "ok_flow_aux_1 c1' SKIP c1'' s1 t1 t1' f f'
            vs1 vs1' vs vs1'' ws1' ws1'' ?cs' ∧
          ok_flow_aux_2 s1 s1' t1 t1' f f' vs1 vs1' ?cs' ∧
          ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws ws1'' ?cs'"
          (is "_ ∧ ?P2 ∧ ?P3")
          using O by fastforce
        hence
         "ok_flow_aux_1 c1' SKIP SKIP s1 t1 t1' f f'
            vs1 vs1' vs vs1'' ws1' ws1'' ?cs'"
          (is ?P1) and ?P2 and ?P3 by auto
        obtain c2' and t2 and vs2' and ws2' where
         "ok_flow_aux_1 c2 c'' c2' s1' t1' t2 f f'
            vs vs1'' vs2 vs2' ws1'' ws2' ?cs'' ∧
          ok_flow_aux_2 s1' s2 t1' t2 f f' vs vs1'' ?cs'' ∧
          ok_flow_aux_3 s1' t1' f f' vs vs1'' ws ws1'' ws2 ws2' ?cs''"
          (is "?P1' ∧ ?P2' ∧ ?P3'")
          using Q by fastforce
        hence ?P1' and ?P2' and ?P3' by auto
        show "∃c2' t2 vs2' ws2'.
          ok_flow_aux_1 c' c'' c2' s1 t1 t2 f f'
            vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
          ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
          ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
        proof (rule exI [of _ c2'], rule exI [of _ t2],
         rule exI [of _ vs2'], rule exI [of _ ws2'])
          {
            fix S
            assume
              R: "S ≠ {}" and
              S: "S ⊆ {x. s1 = t1 (⊆ sources_aux (?cs' @ ?cs'') vs1 s1 f x)}" and
              T: "f = f' (⊆ vs1, vs1',
                ⋃ {tags_aux (?cs' @ ?cs'') vs1 s1 f x | x. x ∈ S})"
                (is "_ = _ (⊆ _, _, ?T)")
            have "∀x. sources_aux ?cs' vs1 s1 f x ⊆
              sources_aux (?cs' @ ?cs'') vs1 s1 f x"
              by (blast intro: subsetD [OF sources_aux_append])
            hence "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs' vs1 s1 f x)}"
              using S by blast
            moreover have "⋃ {tags_aux ?cs' vs1 s1 f x | x. x ∈ S} ⊆ ?T"
              (is "?T' ⊆ _")
              by (blast intro: subsetD [OF tags_aux_append])
            with T have "f = f' (⊆ vs1, vs1', ?T')"
              by (rule eq_streams_subset)
            ultimately have
             "(c1', t1, f', vs1', ws1') →* (SKIP, t1', f', vs1'', ws1'') ∧
              map fst [p←drop (length vs1) vs. fst p ∈ S] =
                map fst [p←drop (length vs1') vs1''. fst p ∈ S]"
              (is "?Q1 ∧ ?Q2")
              using R and `?P1` by simp
            hence ?Q1 and ?Q2 by auto
            have "S ⊆ {x. s1' = t1' (⊆ sources_aux ?cs'' vs s1' f x)}"
              by (rule sources_aux_rhs [OF S T L `?P2`])
            moreover have "f = f' (⊆ vs, vs1'',
              ⋃ {tags_aux ?cs'' vs s1' f x | x. x ∈ S})"
              by (rule tags_aux_rhs [OF S T L `?Q1` `?P1`])
            ultimately have
             "(c2, t1', f', vs1'', ws1'') →* (c2', t2, f', vs2', ws2') ∧
              (c'' = SKIP) = (c2' = SKIP) ∧
              map fst [p←drop (length vs) vs2. fst p ∈ S] =
                map fst [p←drop (length vs1'') vs2'. fst p ∈ S]"
              (is "?Q1' ∧ ?R2 ∧ ?Q2'")
              using R and `?P1'` by simp
            hence ?Q1' and ?R2 and ?Q2' by auto
            from I and `?Q1` and `?Q1'` have
             "(c', t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2')"
              (is ?R1)
              by (blast intro: star_seq2 star_trans)
            moreover have
             "map fst [p←drop (length vs1) vs2. fst p ∈ S] =
                map fst [p←drop (length vs1') vs2'. fst p ∈ S]"
              by (rule small_steps_inputs [OF L M `?Q1` `?Q1'` `?Q2` `?Q2'`])
            ultimately have "?R1 ∧ ?R2 ∧ ?this"
              using `?R2` by simp
          }
          moreover {
            fix S
            assume
              R: "S ≠ {}" and
              S: "S ⊆ {x. s1 = t1 (⊆ sources (?cs' @ ?cs'') vs1 s1 f x)}" and
              T: "f = f' (⊆ vs1, vs1',
                ⋃ {tags (?cs' @ ?cs'') vs1 s1 f x | x. x ∈ S})"
                (is "_ = _ (⊆ _, _, ?T)")
            have "∀x. sources_aux (?cs' @ ?cs'') vs1 s1 f x ⊆
              sources (?cs' @ ?cs'') vs1 s1 f x"
              by (blast intro: subsetD [OF sources_aux_sources])
            moreover have "∀x. sources_aux ?cs' vs1 s1 f x ⊆
              sources_aux (?cs' @ ?cs'') vs1 s1 f x"
              by (blast intro: subsetD [OF sources_aux_append])
            ultimately have U: "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs' vs1 s1 f x)}"
              using S by blast
            have "⋃ {tags_aux (?cs' @ ?cs'') vs1 s1 f x | x. x ∈ S} ⊆ ?T"
              (is "?T' ⊆ _")
              by (blast intro: subsetD [OF tags_aux_tags])
            moreover have "⋃ {tags_aux ?cs' vs1 s1 f x | x. x ∈ S} ⊆ ?T'"
              (is "?T'' ⊆ _")
              by (blast intro: subsetD [OF tags_aux_append])
            ultimately have "?T'' ⊆ ?T"
              by simp
            with T have "f = f' (⊆ vs1, vs1', ?T'')"
              by (rule eq_streams_subset)
            hence V: "(c1', t1, f', vs1', ws1') →* (SKIP, t1', f', vs1'', ws1'')"
              using R and U and `?P1` by simp
            have "S ⊆ {x. s1' = t1' (⊆ sources ?cs'' vs s1' f x)}"
              by (rule sources_rhs [OF S T L `?P2`])
            moreover have "f = f' (⊆ vs, vs1'',
              ⋃ {tags ?cs'' vs s1' f x | x. x ∈ S})"
              by (rule tags_rhs [OF S T L V `?P1`])
            ultimately have "s2 = t2 (⊆ S)"
              using `?P2'` by blast
          }
          moreover {
            fix S
            assume
              R: "S ≠ {}" and
              S: "S ⊆ {x. s1 = t1 (⊆ sources_out (?cs' @ ?cs'') vs1 s1 f x)}" and
              T: "f = f' (⊆ vs1, vs1',
                ⋃ {tags_out (?cs' @ ?cs'') vs1 s1 f x | x. x ∈ S})"
                (is "_ = _ (⊆ _, _, ?T)")
            have U: "∀x. sources_aux (?cs' @ ?cs'') vs1 s1 f x ⊆
              sources_out (?cs' @ ?cs'') vs1 s1 f x"
              by (blast intro: subsetD [OF sources_aux_sources_out])
            moreover have "∀x. sources_aux ?cs' vs1 s1 f x ⊆
              sources_aux (?cs' @ ?cs'') vs1 s1 f x"
              by (blast intro: subsetD [OF sources_aux_append])
            ultimately have V: "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs' vs1 s1 f x)}"
              using S by blast
            have W: "⋃ {tags_aux (?cs' @ ?cs'') vs1 s1 f x | x. x ∈ S} ⊆ ?T"
              (is "?T' ⊆ _")
              by (blast intro: subsetD [OF tags_aux_tags_out])
            moreover have "⋃ {tags_aux ?cs' vs1 s1 f x | x. x ∈ S} ⊆ ?T'"
              (is "?T'' ⊆ _")
              by (blast intro: subsetD [OF tags_aux_append])
            ultimately have "?T'' ⊆ ?T"
              by simp
            with T have "f = f' (⊆ vs1, vs1', ?T'')"
              by (rule eq_streams_subset)
            hence X: "(c1', t1, f', vs1', ws1') →* (SKIP, t1', f', vs1'', ws1'')"
              using R and V and `?P1` by simp
            have Y: "S ⊆ {x. s1 = t1 (⊆ sources_aux (?cs' @ ?cs'') vs1 s1 f x)}"
              using S and U by blast
            have Z: "f = f' (⊆ vs1, vs1', ?T')"
              using T and W by (rule eq_streams_subset)
            have "S ⊆ {x. s1' = t1' (⊆ sources_aux ?cs'' vs s1' f x)}"
              by (rule sources_aux_rhs [OF Y Z L `?P2`])
            moreover have "f = f' (⊆ vs, vs1'',
              ⋃ {tags_aux ?cs'' vs s1' f x | x. x ∈ S})"
              by (rule tags_aux_rhs [OF Y Z L X `?P1`])
            ultimately have AA:
             "(c2, t1', f', vs1'', ws1'') →* (c2', t2, f', vs2', ws2')"
              using R and `?P1'` by simp
            have "∀x. sources_out ?cs' vs1 s1 f x ⊆
              sources_out (?cs' @ ?cs'') vs1 s1 f x"
              by (blast intro: subsetD [OF sources_out_append])
            hence "S ⊆ {x. s1 = t1 (⊆ sources_out ?cs' vs1 s1 f x)}"
              using S by blast
            moreover have "⋃ {tags_out ?cs' vs1 s1 f x | x. x ∈ S} ⊆ ?T"
              (is "?T' ⊆ _")
              by (blast intro: subsetD [OF tags_out_append])
            with T have "f = f' (⊆ vs1, vs1', ?T')"
              by (rule eq_streams_subset)
            ultimately have AB: "[p←drop (length ws1) ws. fst p ∈ S] =
              [p←drop (length ws1') ws1''. fst p ∈ S]"
              using R and `?P3` by simp
            have "S ⊆ {x. s1' = t1' (⊆ sources_out ?cs'' vs s1' f x)}"
              by (rule sources_out_rhs [OF S T L `?P2`])
            moreover have "f = f' (⊆ vs, vs1'',
              ⋃ {tags_out ?cs'' vs s1' f x | x. x ∈ S})"
              by (rule tags_out_rhs [OF S T L X `?P1`])
            ultimately have "[p←drop (length ws) ws2. fst p ∈ S] =
              [p←drop (length ws1'') ws2'. fst p ∈ S]"
              using R and `?P3'` by simp
            hence "[p←drop (length ws1) ws2. fst p ∈ S] =
              [p←drop (length ws1') ws2'. fst p ∈ S]"
              by (rule small_steps_outputs [OF L M X AA AB])
          }
          ultimately show
           "ok_flow_aux_1 c' c'' c2' s1 t1 t2 f f'
              vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
            ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
            ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
            using N by auto
        qed
      qed (simp add: no_upd_append N O Q)
    qed
  next
    fix s' p cfs cfs'
    assume I: "(c1, s, f, vs0, ws0) →*{cfs} (SKIP, s', p)"
    hence "(c1, s, f, vs0, ws0) ⇒ (s', p)"
      by (auto dest: small_stepsl_steps simp: big_iff_small)
    hence J: "s' ∈ Univ B (⊆ state ∩ Y)"
      using G and D by (rule ctyping2_approx)
    assume "(c2, s', p) →*{cfs'} (c', s1, f, vs1, ws1)"
    moreover obtain vs and ws where "p = (f, vs, ws)"
      using I by (blast dest: small_stepsl_stream)
    ultimately have K: "(c2, s', f, vs, ws) →*{cfs'} (c', s1, f, vs1, ws1)"
      by simp
    show ?thesis
      using C [OF G _ H J K F] by simp
  qed
qed

lemma ctyping2_correct_aux_or:
  assumes
    A: "(U, v) ⊨ c1 OR c2 (⊆ A, X) = Some (C, Y)" and
    B: "⋀C Y c' c'' s s1 s2 vs0 vs1 vs2 ws0 ws1 ws2 cfs1 cfs2.
      (U, v) ⊨ c1 (⊆ A, X) = Some (C, Y) ⟹
      s ∈ Univ A (⊆ state ∩ X) ⟹
      (c1, s, f, vs0, ws0) →*{cfs1} (c', s1, f, vs1, ws1) ⟹
      (c', s1, f, vs1, ws1) →*{cfs2} (c'', s2, f, vs2, ws2) ⟹
        ok_flow_aux U c' c'' s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)" and
    C: "⋀C Y c' c'' s s1 s2 vs0 vs1 vs2 ws0 ws1 ws2 cfs1 cfs2.
      (U, v) ⊨ c2 (⊆ A, X) = Some (C, Y) ⟹
      s ∈ Univ A (⊆ state ∩ X) ⟹
      (c2, s, f, vs0, ws0) →*{cfs1} (c', s1, f, vs1, ws1) ⟹
      (c', s1, f, vs1, ws1) →*{cfs2} (c'', s2, f, vs2, ws2) ⟹
        ok_flow_aux U c' c'' s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)" and
    D: "s ∈ Univ A (⊆ state ∩ X)" and
    E: "(c1 OR c2, s, f, vs0, ws0) →*{cfs1} (c', s1, f, vs1, ws1)" and
    F: "(c', s1, f, vs1, ws1) →*{cfs2} (c'', s2, f, vs2, ws2)"
  shows "ok_flow_aux U c' c'' s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)"
proof -
  from A obtain C1 and Y1 and C2 and Y2 where
    G: "(U, v) ⊨ c1 (⊆ A, X) = Some (C1, Y1)" and
    H: "(U, v) ⊨ c2 (⊆ A, X) = Some (C2, Y2)"
    by (auto split: option.split_asm)
  have
   "(c', s1, f, vs1, ws1) = (c1 OR c2, s, f, vs0, ws0) ∨
    (c1, s, f, vs0, ws0) →*{tl cfs1} (c', s1, f, vs1, ws1) ∨
    (c2, s, f, vs0, ws0) →*{tl cfs1} (c', s1, f, vs1, ws1)"
    (is "?P ∨ ?Q ∨ ?R")
    using E by (blast dest: small_stepsl_or)
  thus ?thesis
  proof (rule disjE, erule_tac [2] disjE)
    assume ?P
    hence "(c1 OR c2, s, f, vs0, ws0) →*{cfs2} (c'', s2, f, vs2, ws2)"
      using F by simp
    hence
     "(c'', s2, f, vs2, ws2) = (c1 OR c2, s, f, vs0, ws0) ∧
        flow cfs2 = [] ∨
      (c1, s, f, vs0, ws0) →*{tl cfs2} (c'', s2, f, vs2, ws2) ∧
        flow cfs2 = flow (tl cfs2) ∨
      (c2, s, f, vs0, ws0) →*{tl cfs2} (c'', s2, f, vs2, ws2) ∧
        flow cfs2 = flow (tl cfs2)"
      (is "?P' ∨ _")
      by (rule small_stepsl_or)
    thus ?thesis
    proof (rule disjE, erule_tac [2] disjE, erule_tac [2-3] conjE)
      assume ?P'
      with `?P` show ?thesis
        by fastforce
    next
      assume
        I: "(c1, s, f, vs0, ws0) →*{tl cfs2} (c'', s2, f, vs2, ws2)" and
        J: "flow cfs2 = flow (tl cfs2)"
          (is "?cs = ?cs'")
      have K: "(c1, s, f, vs0, ws0) →*{[]} (c1, s, f, vs0, ws0)"
        by simp
      hence L: "ok_flow_aux U c1 c'' s s2 f vs0 vs2 ws0 ws2 ?cs'"
        by (rule B [OF G D _ I])
      show ?thesis
      proof (rule conjI, clarify)
        fix t1 f' vs1' ws1'
        obtain c2' and t2 and vs2' and ws2' where
         "ok_flow_aux_1 c1 c'' c2' s t1 t2 f f'
            vs0 vs1' vs2 vs2' ws1' ws2' ?cs' ∧
          ok_flow_aux_2 s s2 t1 t2 f f' vs0 vs1' ?cs' ∧
          ok_flow_aux_3 s t1 f f' vs0 vs1' ws0 ws1' ws2 ws2' ?cs'"
          (is "?P1 ∧ ?P2 ∧ ?P3")
          using L by fastforce
        hence ?P1 and ?P2 and ?P3 by auto
        show "∃c2' t2 vs2' ws2'.
          ok_flow_aux_1 c' c'' c2' s1 t1 t2 f f'
            vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
          ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
          ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
        proof (rule exI [of _ "c2'"], rule exI [of _ t2],
         rule exI [of _ vs2'], rule exI [of _ ws2'])
          {
            fix S
            assume
             "S ≠ {}" and
             "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs' vs1 s1 f x)}" and
             "f = f' (⊆ vs1, vs1', ⋃ {tags_aux ?cs' vs1 s1 f x | x. x ∈ S})"
            hence
             "(c1, t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2') ∧
              (c'' = SKIP) = (c2' = SKIP) ∧
              map fst [p←drop (length vs1) vs2. fst p ∈ S] =
                map fst [p←drop (length vs1') vs2'. fst p ∈ S]"
              (is "?Q1 ∧ ?Q2 ∧ ?Q3")
              using `?P` and `?P1` by simp
            hence ?Q1 and ?Q2 and ?Q3 by auto
            moreover have "(c1 OR c2, t1, f', vs1', ws1') →
              (c1, t1, f', vs1', ws1')" ..
            hence "(c', t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2')"
              using `?P` and `?Q1` by (blast intro: star_trans)
            ultimately have "?this ∧ ?Q2 ∧ ?Q3"
              by simp
          }
          moreover {
            fix S
            assume
             "S ⊆ {x. s1 = t1 (⊆ sources ?cs' vs1 s1 f x)}" and
             "f = f' (⊆ vs1, vs1', ⋃ {tags ?cs' vs1 s1 f x | x. x ∈ S})"
            hence "s2 = t2 (⊆ S)"
              using `?P` and `?P2` by blast
          }
          moreover {
            fix S
            assume
             "S ≠ {}" and
             "S ⊆ {x. s1 = t1 (⊆ sources_out ?cs' vs1 s1 f x)}" and
             "f = f' (⊆ vs1, vs1', ⋃ {tags_out ?cs' vs1 s1 f x | x. x ∈ S})"
            hence "[p←drop (length ws1) ws2. fst p ∈ S] =
              [p←drop (length ws1') ws2'. fst p ∈ S]"
              using `?P` and `?P3` by simp
          }
          ultimately show
           "ok_flow_aux_1 c' c'' c2' s1 t1 t2 f f'
              vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
            ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
            ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
            using J by auto
        qed
      qed (simp add: B [OF G D K I] J)
    next
      assume
        I: "(c2, s, f, vs0, ws0) →*{tl cfs2} (c'', s2, f, vs2, ws2)" and
        J: "flow cfs2 = flow (tl cfs2)"
          (is "?cs = ?cs'")
      have K: "(c2, s, f, vs0, ws0) →*{[]} (c2, s, f, vs0, ws0)"
        by simp
      hence L: "ok_flow_aux U c2 c'' s s2 f vs0 vs2 ws0 ws2 ?cs'"
        by (rule C [OF H D _ I])
      show ?thesis
      proof (rule conjI, clarify)
        fix t1 f' vs1' ws1'
        obtain c2' and t2 and vs2' and ws2' where
         "ok_flow_aux_1 c2 c'' c2' s t1 t2 f f'
            vs0 vs1' vs2 vs2' ws1' ws2' ?cs' ∧
          ok_flow_aux_2 s s2 t1 t2 f f' vs0 vs1' ?cs' ∧
          ok_flow_aux_3 s t1 f f' vs0 vs1' ws0 ws1' ws2 ws2' ?cs'"
          (is "?P1 ∧ ?P2 ∧ ?P3")
          using L by fastforce
        hence ?P1 and ?P2 and ?P3 by auto
        show "∃c2' t2 vs2' ws2'.
          ok_flow_aux_1 c' c'' c2' s1 t1 t2 f f'
            vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
          ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
          ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
        proof (rule exI [of _ "c2'"], rule exI [of _ t2],
         rule exI [of _ vs2'], rule exI [of _ ws2'])
          {
            fix S
            assume
             "S ≠ {}" and
             "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs' vs1 s1 f x)}" and
             "f = f' (⊆ vs1, vs1', ⋃ {tags_aux ?cs' vs1 s1 f x | x. x ∈ S})"
            hence
             "(c2, t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2') ∧
              (c'' = SKIP) = (c2' = SKIP) ∧
              map fst [p←drop (length vs1) vs2. fst p ∈ S] =
                map fst [p←drop (length vs1') vs2'. fst p ∈ S]"
              (is "?Q1 ∧ ?Q2 ∧ ?Q3")
              using `?P` and `?P1` by simp
            hence ?Q1 and ?Q2 and ?Q3 by auto
            moreover have "(c1 OR c2, t1, f', vs1', ws1') →
              (c2, t1, f', vs1', ws1')" ..
            hence "(c', t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2')"
              using `?P` and `?Q1` by (blast intro: star_trans)
            ultimately have "?this ∧ ?Q2 ∧ ?Q3"
              by simp
          }
          moreover {
            fix S
            assume
             "S ⊆ {x. s1 = t1 (⊆ sources ?cs' vs1 s1 f x)}" and
             "f = f' (⊆ vs1, vs1', ⋃ {tags ?cs' vs1 s1 f x | x. x ∈ S})"
            hence "s2 = t2 (⊆ S)"
              using `?P` and `?P2` by blast
          }
          moreover {
            fix S
            assume
             "S ≠ {}" and
             "S ⊆ {x. s1 = t1 (⊆ sources_out ?cs' vs1 s1 f x)}" and
             "f = f' (⊆ vs1, vs1', ⋃ {tags_out ?cs' vs1 s1 f x | x. x ∈ S})"
            hence "[p←drop (length ws1) ws2. fst p ∈ S] =
              [p←drop (length ws1') ws2'. fst p ∈ S]"
              using `?P` and `?P3` by simp
          }
          ultimately show
           "ok_flow_aux_1 c' c'' c2' s1 t1 t2 f f'
              vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
            ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
            ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
            using J by auto
        qed
      qed (simp add: C [OF H D K I] J)
    qed
  next
    assume ?Q
    thus ?thesis
      by (rule B [OF G D _ F])
  next
    assume ?R
    thus ?thesis
      by (rule C [OF H D _ F])
  qed
qed

lemma ctyping2_correct_aux_if:
  assumes
    A: "(U, v) ⊨ IF b THEN c1 ELSE c2 (⊆ A, X) = Some (C, Y)" and
    B: "⋀U' p B1 B2 C1 Y1 c' c'' s s1 s2 vs0 vs1 vs2 ws0 ws1 ws2 cfs1 cfs2.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B1, B2) = p ⟹
      (U', v) ⊨ c1 (⊆ B1, X) = Some (C1, Y1) ⟹
      s ∈ Univ B1 (⊆ state ∩ X) ⟹
      (c1, s, f, vs0, ws0) →*{cfs1} (c', s1, f, vs1, ws1) ⟹
      (c', s1, f, vs1, ws1) →*{cfs2} (c'', s2, f, vs2, ws2) ⟹
        ok_flow_aux U' c' c'' s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)" and
    C: "⋀U' p B1 B2 C2 Y2 c' c'' s s1 s2 vs0 vs1 vs2 ws0 ws1 ws2 cfs1 cfs2.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B1, B2) = p ⟹
      (U', v) ⊨ c2 (⊆ B2, X) = Some (C2, Y2) ⟹
      s ∈ Univ B2 (⊆ state ∩ X) ⟹
      (c2, s, f, vs0, ws0) →*{cfs1} (c', s1, f, vs1, ws1) ⟹
      (c', s1, f, vs1, ws1) →*{cfs2} (c'', s2, f, vs2, ws2) ⟹
        ok_flow_aux U' c' c'' s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)" and
    D: "s ∈ Univ A (⊆ state ∩ X)" and
    E: "(IF b THEN c1 ELSE c2, s, f, vs0, ws0) →*{cfs1}
      (c', s1, f, vs1, ws1)" and
    F: "(c', s1, f, vs1, ws1) →*{cfs2} (c'', s2, f, vs2, ws2)"
  shows "ok_flow_aux U c' c'' s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)"
proof -
  let ?U' = "insert (Univ? A X, bvars b) U"
  from A obtain B1 and B2 and C1 and C2 and Y1 and Y2 where
    G: "⊨ b (⊆ A, X) = (B1, B2)" and
    H: "(?U', v) ⊨ c1 (⊆ B1, X) = Some (C1, Y1)" and
    I: "(?U', v) ⊨ c2 (⊆ B2, X) = Some (C2, Y2)"
    by (auto split: option.split_asm prod.split_asm)
  have
   "(c', s1, f, vs1, ws1) = (IF b THEN c1 ELSE c2, s, f, vs0, ws0) ∨
    bval b s ∧ (c1, s, f, vs0, ws0) →*{tl cfs1} (c', s1, f, vs1, ws1) ∨
    ¬ bval b s ∧ (c2, s, f, vs0, ws0) →*{tl cfs1} (c', s1, f, vs1, ws1)"
    (is "?P ∨ _")
    using E by (blast dest: small_stepsl_if)
  thus ?thesis
  proof (rule disjE, erule_tac [2] disjE, erule_tac [2-3] conjE)
    assume ?P
    hence "(IF b THEN c1 ELSE c2, s, f, vs0, ws0) →*{cfs2}
      (c'', s2, f, vs2, ws2)"
      using F by simp
    hence
     "(c'', s2, f, vs2, ws2) = (IF b THEN c1 ELSE c2, s, f, vs0, ws0) ∧
        flow cfs2 = [] ∨
      bval b s ∧ (c1, s, f, vs0, ws0) →*{tl cfs2} (c'', s2, f, vs2, ws2) ∧
        flow cfs2 = ⟨bvars b⟩ # flow (tl cfs2) ∨
      ¬ bval b s ∧ (c2, s, f, vs0, ws0) →*{tl cfs2} (c'', s2, f, vs2, ws2) ∧
        flow cfs2 = ⟨bvars b⟩ # flow (tl cfs2)"
      (is "?P' ∨ _")
      by (rule small_stepsl_if)
    thus ?thesis
    proof (rule disjE, erule_tac [2] disjE, (erule_tac [2-3] conjE)+)
      assume ?P'
      with `?P` show ?thesis
        by fastforce
    next
      assume
        J: "bval b s" and
        K: "(c1, s, f, vs0, ws0) →*{tl cfs2} (c'', s2, f, vs2, ws2)" and
        L: "flow cfs2 = ⟨bvars b⟩ # flow (tl cfs2)"
          (is "?cs = _ # ?cs'")
      have M: "s ∈ Univ B1 (⊆ state ∩ X)"
        using J by (insert btyping2_approx [OF G D], simp)
      have N: "(c1, s, f, vs0, ws0) →*{[]} (c1, s, f, vs0, ws0)"
        by simp
      show ?thesis
      proof (rule conjI, clarify)
        fix t1 f' vs1' ws1'
        show "∃c2' t2 vs2' ws2'.
          ok_flow_aux_1 c' c'' c2' s1 t1 t2 f f'
            vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
          ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
          ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
        proof (cases "bval b t1")
          assume O: "bval b t1"
          have "ok_flow_aux ?U' c1 c'' s s2 f vs0 vs2 ws0 ws2 ?cs'"
            using B [OF _ _ H M N K] and G by simp
          then obtain c2' and t2 and vs2' and ws2' where
           "ok_flow_aux_1 c1 c'' c2' s t1 t2 f f'
              vs0 vs1' vs2 vs2' ws1' ws2' ?cs' ∧
            ok_flow_aux_2 s s2 t1 t2 f f' vs0 vs1' ?cs' ∧
            ok_flow_aux_3 s t1 f f' vs0 vs1' ws0 ws1' ws2 ws2' ?cs'"
            (is "?P1 ∧ ?P2 ∧ ?P3")
            by fastforce
          hence ?P1 and ?P2 and ?P3 by auto
          show ?thesis
          proof (rule exI [of _ c2'], rule exI [of _ t2],
           rule exI [of _ vs2'], rule exI [of _ ws2'])
            {
              fix S
              assume
                P: "S ≠ {}" and
                Q: "S ⊆ {x. s1 = t1
                  (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x)}" and
                R: "f = f' (⊆ vs1, vs1',
                  ⋃ {tags_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x | x. x ∈ S})"
              have "∀x. sources_aux ?cs' vs1 s1 f x ⊆
                sources_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x"
                by (blast intro: subsetD [OF sources_aux_observe_tl])
              hence "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs' vs1 s1 f x)}"
                using Q by blast
              moreover have "f = f' (⊆ vs1, vs1',
                ⋃ {tags_aux ?cs' vs1 s1 f x | x. x ∈ S})"
                using R by (simp add: tags_aux_observe_tl)
              ultimately have
               "(c1, t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2') ∧
                (c'' = SKIP) = (c2' = SKIP) ∧
                map fst [p←drop (length vs1) vs2. fst p ∈ S] =
                  map fst [p←drop (length vs1') vs2'. fst p ∈ S]"
                (is "?Q1 ∧ ?Q2 ∧ ?Q3")
                using P and `?P` and `?P1` by simp
              hence ?Q1 and ?Q2 and ?Q3 by auto
              moreover have "(IF b THEN c1 ELSE c2, t1, f', vs1', ws1') →
                (c1, t1, f', vs1', ws1')"
                using O ..
              hence "(c', t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2')"
                using `?P` and `?Q1` by (blast intro: star_trans)
              ultimately have "?this ∧ ?Q2 ∧ ?Q3"
                by simp
            }
            moreover {
              fix S
              assume
                P: "S ⊆ {x. s1 = t1
                  (⊆ sources (⟨bvars b⟩ # ?cs') vs1 s1 f x)}" and
                Q: "f = f' (⊆ vs1, vs1',
                  ⋃ {tags (⟨bvars b⟩ # ?cs') vs1 s1 f x | x. x ∈ S})"
              have "∀x. sources ?cs' vs1 s1 f x ⊆
                sources (⟨bvars b⟩ # ?cs') vs1 s1 f x"
                by (blast intro: subsetD [OF sources_observe_tl])
              hence "S ⊆ {x. s1 = t1 (⊆ sources ?cs' vs1 s1 f x)}"
                using P by blast
              moreover have "f = f' (⊆ vs1, vs1',
                ⋃ {tags ?cs' vs1 s1 f x | x. x ∈ S})"
                using Q by (simp add: tags_observe_tl)
              ultimately have "s2 = t2 (⊆ S)"
                using `?P` and `?P2` by blast
            }
            moreover {
              fix S
              assume
                P: "S ≠ {}" and
                Q: "S ⊆ {x. s1 = t1
                  (⊆ sources_out (⟨bvars b⟩ # ?cs') vs1 s1 f x)}" and
                R: "f = f' (⊆ vs1, vs1',
                  ⋃ {tags_out (⟨bvars b⟩ # ?cs') vs1 s1 f x | x. x ∈ S})"
              have "∀x. sources_out ?cs' vs1 s1 f x ⊆
                sources_out (⟨bvars b⟩ # ?cs') vs1 s1 f x"
                by (blast intro: subsetD [OF sources_out_observe_tl])
              hence "S ⊆ {x. s1 = t1 (⊆ sources_out ?cs' vs1 s1 f x)}"
                using Q by blast
              moreover have "f = f' (⊆ vs1, vs1',
                ⋃ {tags_out ?cs' vs1 s1 f x | x. x ∈ S})"
                using R by (simp add: tags_out_observe_tl)
              ultimately have "[p←drop (length ws1) ws2. fst p ∈ S] =
                [p←drop (length ws1') ws2'. fst p ∈ S]"
                using P and `?P` and `?P3` by simp
            }
            ultimately show
             "ok_flow_aux_1 c' c'' c2' s1 t1 t2 f f'
                vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
              ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
              ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
              using L by auto
          qed
        next
          assume O: "¬ bval b t1"
          show ?thesis
          proof (cases "∃S ≠ {}. S ⊆ {x. s1 = t1
           (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x)}")
            from O have "(IF b THEN c1 ELSE c2, t1, f', vs1', ws1') →
              (c2, t1, f', vs1', ws1')" ..
            moreover assume "∃S ≠ {}. S ⊆ {x. s1 = t1
              (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x)}"
            then obtain S where
              P: "S ≠ {}" and
              Q: "S ⊆ {x. s = t1
                (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x)}"
              using `?P` by blast
            have R: "Univ? A X: bvars b ↝| S"
              using Q and D by (rule sources_aux_bval, insert J O, simp)
            have "∃p. (c2, t1, f', vs1', ws1') ⇒ p"
              using I by (rule ctyping2_term, insert P R, auto)
            then obtain t2 and f'' and vs2' and ws2' where
              S: "(c2, t1, f', vs1', ws1') →* (SKIP, t2, f'', vs2', ws2')"
              by (auto simp: big_iff_small)
            ultimately have
             "(c', t1, f', vs1', ws1') →* (SKIP, t2, f', vs2', ws2')"
              (is ?Q1)
              using `?P` by (blast dest: small_steps_stream
               intro: star_trans)
            have T: "(c2, t1, f', vs1', ws1') ⇒ (t2, f'', vs2', ws2')"
              using S by (simp add: big_iff_small)
            show ?thesis
            proof (cases "c'' = SKIP")
              assume "c'' = SKIP"
                (is ?Q2)
              show ?thesis
              proof (rule exI [of _ SKIP], rule exI [of _ t2],
               rule exI [of _ vs2'], rule exI [of _ ws2'])
                {
                  fix S
                  assume "S ⊆ {x. s = t1
                    (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                  hence U: "Univ? A X: bvars b ↝| S"
                    using D by (rule sources_aux_bval, insert J O, simp)
                  hence "[p←drop (length vs1') vs2'. fst p ∈ S] = []"
                    using I and T by (blast dest: ctyping2_confine)
                  moreover have "no_upd ?cs' S"
                    using B [OF _ _ H M N K] and G and U by simp
                  hence "[p←in_flow ?cs' vs1 f. fst p ∈ S] = []"
                    by (rule no_upd_in_flow)
                  moreover have "vs2 = vs0 @ in_flow ?cs' vs0 f"
                    using K by (rule small_stepsl_in_flow)
                  ultimately have "[p←drop (length vs1) vs2. fst p ∈ S] =
                    [p←drop (length vs1') vs2'. fst p ∈ S]"
                    using `?P` by simp
                  hence "?Q1 ∧ ?Q2 ∧ ?this"
                    using `?Q1` and `?Q2` by simp
                }
                moreover {
                  fix S
                  assume U: "S ⊆ {x. s = t1
                    (⊆ sources (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                  moreover have
                   "∀x. sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x ⊆
                      sources (⟨bvars b⟩ # ?cs') vs1 s f x"
                    by (blast intro: subsetD [OF sources_aux_sources])
                  ultimately have "S ⊆ {x. s = t1
                    (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                    by blast
                  hence V: "Univ? A X: bvars b ↝| S"
                    using D by (rule sources_aux_bval, insert J O, simp)
                  hence "t1 = t2 (⊆ S)"
                    using I and T by (blast dest: ctyping2_confine)
                  moreover have W: "no_upd ?cs' S"
                    using B [OF _ _ H M N K] and G and V by simp
                  hence "run_flow ?cs' vs0 s f = s (⊆ S)"
                    by (rule no_upd_run_flow)
                  moreover have "s2 = run_flow ?cs' vs0 s f"
                    using K by (rule small_stepsl_run_flow)
                  moreover have
                   "∀x ∈ S. x ∈ sources (⟨bvars b⟩ # ?cs') vs1 s f x"
                    by (rule no_upd_sources, simp add: W)
                  hence "s = t1 (⊆ S)"
                    using U by blast
                  ultimately have "s2 = t2 (⊆ S)"
                    by simp
                }
                moreover {
                  fix S
                  assume "S ⊆ {x. s = t1
                    (⊆ sources_out (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                  moreover have
                   "∀x. sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x ⊆
                      sources_out (⟨bvars b⟩ # ?cs') vs1 s f x"
                    by (blast intro: subsetD [OF sources_aux_sources_out])
                  ultimately have "S ⊆ {x. s = t1
                    (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                    by blast
                  hence U: "Univ? A X: bvars b ↝| S"
                    using D by (rule sources_aux_bval, insert J O, simp)
                  hence "[p←drop (length ws1') ws2'. fst p ∈ S] = []"
                    using I and T by (blast dest: ctyping2_confine)
                  moreover have "no_upd ?cs' S"
                    using B [OF _ _ H M N K] and G and U by simp
                  hence "[p←out_flow ?cs' vs1 s f. fst p ∈ S] = []"
                    by (rule no_upd_out_flow)
                  moreover have "ws2 = ws0 @ out_flow ?cs' vs0 s f"
                    using K by (rule small_stepsl_out_flow)
                  ultimately have
                   "[p←drop (length ws1) ws2. fst p ∈ S] =
                    [p←drop (length ws1') ws2'. fst p ∈ S]"
                    using `?P` by simp
                }
                ultimately show
                 "ok_flow_aux_1 c' c'' SKIP s1 t1 t2 f f'
                    vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
                  ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
                  ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
                  using L and `?P` by auto
              qed
            next
              assume "c'' ≠ SKIP"
                (is ?Q2)
              show ?thesis
              proof (rule exI [of _ c'], rule exI [of _ t1],
               rule exI [of _ vs1'], rule exI [of _ ws1'])
                {
                  fix S
                  assume "S ⊆ {x. s = t1
                    (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                  hence "Univ? A X: bvars b ↝| S"
                    using D by (rule sources_aux_bval, insert J O, simp)
                  hence "no_upd ?cs' S"
                    using B [OF _ _ H M N K] and G by simp
                  hence "[p←in_flow ?cs' vs1 f. fst p ∈ S] = []"
                    by (rule no_upd_in_flow)
                  moreover have "vs2 = vs0 @ in_flow ?cs' vs0 f"
                    using K by (rule small_stepsl_in_flow)
                  ultimately have
                   "[p←drop (length vs1) vs2. fst p ∈ S] = []"
                    using `?P` by simp
                  hence "?Q2 ∧ ?this"
                    using `?Q2` by simp
                }
                moreover {
                  fix S
                  assume U: "S ⊆ {x. s = t1
                    (⊆ sources (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                  moreover have
                   "∀x. sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x ⊆
                      sources (⟨bvars b⟩ # ?cs') vs1 s f x"
                    by (blast intro: subsetD [OF sources_aux_sources])
                  ultimately have "S ⊆ {x. s = t1
                    (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                    by blast
                  hence "Univ? A X: bvars b ↝| S"
                    using D by (rule sources_aux_bval, insert J O, simp)
                  hence V: "no_upd ?cs' S"
                    using B [OF _ _ H M N K] and G by simp
                  hence "run_flow ?cs' vs0 s f = s (⊆ S)"
                    by (rule no_upd_run_flow)
                  moreover have "s2 = run_flow ?cs' vs0 s f"
                    using K by (rule small_stepsl_run_flow)
                  moreover have
                   "∀x ∈ S. x ∈ sources (⟨bvars b⟩ # ?cs') vs1 s f x"
                    by (rule no_upd_sources, simp add: V)
                  hence "s = t1 (⊆ S)"
                    using U by blast
                  ultimately have "s2 = t1 (⊆ S)"
                    by simp
                }
                moreover {
                  fix S
                  assume "S ⊆ {x. s = t1
                    (⊆ sources_out (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                  moreover have
                   "∀x. sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x ⊆
                      sources_out (⟨bvars b⟩ # ?cs') vs1 s f x"
                    by (blast intro: subsetD [OF sources_aux_sources_out])
                  ultimately have "S ⊆ {x. s = t1
                    (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                    by blast
                  hence "Univ? A X: bvars b ↝| S"
                    using D by (rule sources_aux_bval, insert J O, simp)
                  hence "no_upd ?cs' S"
                    using B [OF _ _ H M N K] and G by simp
                  hence "[p←out_flow ?cs' vs1 s f. fst p ∈ S] = []"
                    by (rule no_upd_out_flow)
                  moreover have "ws2 = ws0 @ out_flow ?cs' vs0 s f"
                    using K by (rule small_stepsl_out_flow)
                  ultimately have
                   "[p←drop (length ws1) ws2. fst p ∈ S] = []"
                    using `?P` by simp
                }
                ultimately show
                 "ok_flow_aux_1 c' c'' c' s1 t1 t1 f f'
                    vs1 vs1' vs2 vs1' ws1' ws1' ?cs ∧
                  ok_flow_aux_2 s1 s2 t1 t1 f f' vs1 vs1' ?cs ∧
                  ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws1' ?cs"
                  using L and `?P` by auto
              qed
            qed
          next
            assume "∄S. S ≠ {} ∧ S ⊆ {x. s1 = t1
              (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x)}"
            hence O: "∀c2' t2 vs2' ws2'.
              ok_flow_aux_1 c' c'' c2' s1 t1 t2 f f'
                vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
              ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
              ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
              using L by (auto intro!: ok_flow_aux_degen)
            show ?thesis
              by (rule exI [of _ SKIP], rule exI [of _ "λx. 0"],
               rule exI [of _ "[]"], rule exI [of _ "[]"],
               simp add: O [rule_format, of SKIP "λx. 0" "[]" "[]"])
          qed
        qed
      qed (simp add: B [OF _ _ H M N K] G L)
    next
      assume
        J: "¬ bval b s" and
        K: "(c2, s, f, vs0, ws0) →*{tl cfs2} (c'', s2, f, vs2, ws2)" and
        L: "flow cfs2 = ⟨bvars b⟩ # flow (tl cfs2)"
          (is "?cs = _ # ?cs'")
      have M: "s ∈ Univ B2 (⊆ state ∩ X)"
        using J by (insert btyping2_approx [OF G D], simp)
      have N: "(c2, s, f, vs0, ws0) →*{[]} (c2, s, f, vs0, ws0)"
        by simp
      show ?thesis
      proof (rule conjI, clarify)
        fix t1 f' vs1' ws1'
        show "∃c2' t2 vs2' ws2'.
          ok_flow_aux_1 c' c'' c2' s1 t1 t2 f f'
            vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
          ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
          ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
        proof (cases "bval b t1", cases "∃S ≠ {}.
         S ⊆ {x. s1 = t1 (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x)}")
          assume O: "¬ bval b t1"
          have "ok_flow_aux ?U' c2 c'' s s2 f vs0 vs2 ws0 ws2 ?cs'"
            using C [OF _ _ I M N K] and G by simp
          then obtain c2' and t2 and vs2' and ws2' where
           "ok_flow_aux_1 c2 c'' c2' s t1 t2 f f'
              vs0 vs1' vs2 vs2' ws1' ws2' ?cs' ∧
            ok_flow_aux_2 s s2 t1 t2 f f' vs0 vs1' ?cs' ∧
            ok_flow_aux_3 s t1 f f' vs0 vs1' ws0 ws1' ws2 ws2' ?cs'"
            (is "?P1 ∧ ?P2 ∧ ?P3")
            by fastforce
          hence ?P1 and ?P2 and ?P3 by auto
          show ?thesis
          proof (rule exI [of _ c2'], rule exI [of _ t2],
           rule exI [of _ vs2'], rule exI [of _ ws2'])
            {
              fix S
              assume
                P: "S ≠ {}" and
                Q: "S ⊆ {x. s1 = t1
                  (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x)}" and
                R: "f = f' (⊆ vs1, vs1',
                  ⋃ {tags_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x | x. x ∈ S})"
              have "∀x. sources_aux ?cs' vs1 s1 f x ⊆
                sources_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x"
                by (blast intro: subsetD [OF sources_aux_observe_tl])
              hence "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs' vs1 s1 f x)}"
                using Q by blast
              moreover have "f = f' (⊆ vs1, vs1',
                ⋃ {tags_aux ?cs' vs1 s1 f x | x. x ∈ S})"
                using R by (simp add: tags_aux_observe_tl)
              ultimately have
               "(c2, t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2') ∧
                (c'' = SKIP) = (c2' = SKIP) ∧
                map fst [p←drop (length vs1) vs2. fst p ∈ S] =
                  map fst [p←drop (length vs1') vs2'. fst p ∈ S]"
                (is "?Q1 ∧ ?Q2 ∧ ?Q3")
                using P and `?P` and `?P1` by simp
              hence ?Q1 and ?Q2 and ?Q3 by auto
              moreover have "(IF b THEN c1 ELSE c2, t1, f', vs1', ws1') →
                (c2, t1, f', vs1', ws1')"
                using O ..
              hence "(c', t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2')"
                using `?P` and `?Q1` by (blast intro: star_trans)
              ultimately have "?this ∧ ?Q2 ∧ ?Q3"
                by simp
            }
            moreover {
              fix S
              assume
                P: "S ⊆ {x. s1 = t1
                  (⊆ sources (⟨bvars b⟩ # ?cs') vs1 s1 f x)}" and
                Q: "f = f' (⊆ vs1, vs1',
                  ⋃ {tags (⟨bvars b⟩ # ?cs') vs1 s1 f x | x. x ∈ S})"
              have "∀x. sources ?cs' vs1 s1 f x ⊆
                sources (⟨bvars b⟩ # ?cs') vs1 s1 f x"
                by (blast intro: subsetD [OF sources_observe_tl])
              hence "S ⊆ {x. s1 = t1 (⊆ sources ?cs' vs1 s1 f x)}"
                using P by blast
              moreover have "f = f' (⊆ vs1, vs1',
                ⋃ {tags ?cs' vs1 s1 f x | x. x ∈ S})"
                using Q by (simp add: tags_observe_tl)
              ultimately have "s2 = t2 (⊆ S)"
                using `?P` and `?P2` by blast
            }
            moreover {
              fix S
              assume
                P: "S ≠ {}" and
                Q: "S ⊆ {x. s1 = t1
                  (⊆ sources_out (⟨bvars b⟩ # ?cs') vs1 s1 f x)}" and
                R: "f = f' (⊆ vs1, vs1',
                  ⋃ {tags_out (⟨bvars b⟩ # ?cs') vs1 s1 f x | x. x ∈ S})"
              have "∀x. sources_out ?cs' vs1 s1 f x ⊆
                sources_out (⟨bvars b⟩ # ?cs') vs1 s1 f x"
                by (blast intro: subsetD [OF sources_out_observe_tl])
              hence "S ⊆ {x. s1 = t1 (⊆ sources_out ?cs' vs1 s1 f x)}"
                using Q by blast
              moreover have "f = f' (⊆ vs1, vs1',
                ⋃ {tags_out ?cs' vs1 s1 f x | x. x ∈ S})"
                using R by (simp add: tags_out_observe_tl)
              ultimately have "[p←drop (length ws1) ws2. fst p ∈ S] =
                [p←drop (length ws1') ws2'. fst p ∈ S]"
                using P and `?P` and `?P3` by simp
            }
            ultimately show
             "ok_flow_aux_1 c' c'' c2' s1 t1 t2 f f'
                vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
              ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
              ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
              using L by auto
          qed
        next
          assume O: "bval b t1"
          hence "(IF b THEN c1 ELSE c2, t1, f', vs1', ws1') →
            (c1, t1, f', vs1', ws1')" ..
          moreover assume "∃S ≠ {}.
            S ⊆ {x. s1 = t1 (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x)}"
          then obtain S where
            P: "S ≠ {}" and
            Q: "S ⊆ {x. s = t1 (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x)}"
            using `?P` by blast
          have R: "Univ? A X: bvars b ↝| S"
            using Q and D by (rule sources_aux_bval, insert J O, simp)
          have "∃p. (c1, t1, f', vs1', ws1') ⇒ p"
            using H by (rule ctyping2_term, insert P R, auto)
          then obtain t2 and f'' and vs2' and ws2' where
            S: "(c1, t1, f', vs1', ws1') →* (SKIP, t2, f'', vs2', ws2')"
            by (auto simp: big_iff_small)
          ultimately have
           "(c', t1, f', vs1', ws1') →* (SKIP, t2, f', vs2', ws2')"
            (is ?Q1)
            using `?P` by (blast dest: small_steps_stream intro: star_trans)
          have T: "(c1, t1, f', vs1', ws1') ⇒ (t2, f'', vs2', ws2')"
            using S by (simp add: big_iff_small)
          show ?thesis
          proof (cases "c'' = SKIP")
            assume "c'' = SKIP"
              (is ?Q2)
            show ?thesis
            proof (rule exI [of _ SKIP], rule exI [of _ t2],
             rule exI [of _ vs2'], rule exI [of _ ws2'])
              {
                fix S
                assume "S ⊆ {x. s = t1
                  (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                hence U: "Univ? A X: bvars b ↝| S"
                  using D by (rule sources_aux_bval, insert J O, simp)
                hence "[p←drop (length vs1') vs2'. fst p ∈ S] = []"
                  using H and T by (blast dest: ctyping2_confine)
                moreover have "no_upd ?cs' S"
                  using C [OF _ _ I M N K] and G and U by simp
                hence "[p←in_flow ?cs' vs1 f. fst p ∈ S] = []"
                  by (rule no_upd_in_flow)
                moreover have "vs2 = vs0 @ in_flow ?cs' vs0 f"
                  using K by (rule small_stepsl_in_flow)
                ultimately have "[p←drop (length vs1) vs2. fst p ∈ S] =
                  [p←drop (length vs1') vs2'. fst p ∈ S]"
                  using `?P` by simp
                hence "?Q1 ∧ ?Q2 ∧ ?this"
                  using `?Q1` and `?Q2` by simp
              }
              moreover {
                fix S
                assume U: "S ⊆ {x. s = t1
                  (⊆ sources (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                moreover have "∀x. sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x ⊆
                  sources (⟨bvars b⟩ # ?cs') vs1 s f x"
                  by (blast intro: subsetD [OF sources_aux_sources])
                ultimately have "S ⊆ {x. s = t1
                  (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                  by blast
                hence V: "Univ? A X: bvars b ↝| S"
                  using D by (rule sources_aux_bval, insert J O, simp)
                hence "t1 = t2 (⊆ S)"
                  using H and T by (blast dest: ctyping2_confine)
                moreover have W: "no_upd ?cs' S"
                  using C [OF _ _ I M N K] and G and V by simp
                hence "run_flow ?cs' vs0 s f = s (⊆ S)"
                  by (rule no_upd_run_flow)
                moreover have "s2 = run_flow ?cs' vs0 s f"
                  using K by (rule small_stepsl_run_flow)
                moreover have "∀x ∈ S. x ∈ sources (⟨bvars b⟩ # ?cs') vs1 s f x"
                  by (rule no_upd_sources, simp add: W)
                hence "s = t1 (⊆ S)"
                  using U by blast
                ultimately have "s2 = t2 (⊆ S)"
                  by simp
              }
              moreover {
                fix S
                assume "S ⊆ {x. s = t1
                  (⊆ sources_out (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                moreover have "∀x. sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x ⊆
                  sources_out (⟨bvars b⟩ # ?cs') vs1 s f x"
                  by (blast intro: subsetD [OF sources_aux_sources_out])
                ultimately have "S ⊆ {x. s = t1
                  (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                  by blast
                hence U: "Univ? A X: bvars b ↝| S"
                  using D by (rule sources_aux_bval, insert J O, simp)
                hence "[p←drop (length ws1') ws2'. fst p ∈ S] = []"
                  using H and T by (blast dest: ctyping2_confine)
                moreover have "no_upd ?cs' S"
                  using C [OF _ _ I M N K] and G and U by simp
                hence "[p←out_flow ?cs' vs1 s f. fst p ∈ S] = []"
                  by (rule no_upd_out_flow)
                moreover have "ws2 = ws0 @ out_flow ?cs' vs0 s f"
                  using K by (rule small_stepsl_out_flow)
                ultimately have
                 "[p←drop (length ws1) ws2. fst p ∈ S] =
                  [p←drop (length ws1') ws2'. fst p ∈ S]"
                  using `?P` by simp
              }
              ultimately show
               "ok_flow_aux_1 c' c'' SKIP s1 t1 t2 f f'
                  vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
                ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
                ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
                using L and `?P` by auto
            qed
          next
            assume "c'' ≠ SKIP"
              (is ?Q2)
            show ?thesis
            proof (rule exI [of _ c'], rule exI [of _ t1],
             rule exI [of _ vs1'], rule exI [of _ ws1'])
              {
                fix S
                assume "S ⊆ {x. s = t1
                  (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                hence "Univ? A X: bvars b ↝| S"
                  using D by (rule sources_aux_bval, insert J O, simp)
                hence "no_upd ?cs' S"
                  using C [OF _ _ I M N K] and G by simp
                hence "[p←in_flow ?cs' vs1 f. fst p ∈ S] = []"
                  by (rule no_upd_in_flow)
                moreover have "vs2 = vs0 @ in_flow ?cs' vs0 f"
                  using K by (rule small_stepsl_in_flow)
                ultimately have "[p←drop (length vs1) vs2. fst p ∈ S] = []"
                  using `?P` by simp
                hence "?Q2 ∧ ?this"
                  using `?Q2` by simp
              }
              moreover {
                fix S
                assume U: "S ⊆ {x. s = t1
                  (⊆ sources (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                moreover have "∀x. sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x ⊆
                  sources (⟨bvars b⟩ # ?cs') vs1 s f x"
                  by (blast intro: subsetD [OF sources_aux_sources])
                ultimately have "S ⊆ {x. s = t1
                  (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                  by blast
                hence "Univ? A X: bvars b ↝| S"
                  using D by (rule sources_aux_bval, insert J O, simp)
                hence V: "no_upd ?cs' S"
                  using C [OF _ _ I M N K] and G by simp
                hence "run_flow ?cs' vs0 s f = s (⊆ S)"
                  by (rule no_upd_run_flow)
                moreover have "s2 = run_flow ?cs' vs0 s f"
                  using K by (rule small_stepsl_run_flow)
                moreover have "∀x ∈ S. x ∈ sources (⟨bvars b⟩ # ?cs') vs1 s f x"
                  by (rule no_upd_sources, simp add: V)
                hence "s = t1 (⊆ S)"
                  using U by blast
                ultimately have "s2 = t1 (⊆ S)"
                  by simp
              }
              moreover {
                fix S
                assume "S ⊆ {x. s = t1
                  (⊆ sources_out (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                moreover have "∀x. sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x ⊆
                  sources_out (⟨bvars b⟩ # ?cs') vs1 s f x"
                  by (blast intro: subsetD [OF sources_aux_sources_out])
                ultimately have "S ⊆ {x. s = t1
                  (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s f x)}"
                  by blast
                hence "Univ? A X: bvars b ↝| S"
                  using D by (rule sources_aux_bval, insert J O, simp)
                hence "no_upd ?cs' S"
                  using C [OF _ _ I M N K] and G by simp
                hence "[p←out_flow ?cs' vs1 s f. fst p ∈ S] = []"
                  by (rule no_upd_out_flow)
                moreover have "ws2 = ws0 @ out_flow ?cs' vs0 s f"
                  using K by (rule small_stepsl_out_flow)
                ultimately have "[p←drop (length ws1) ws2. fst p ∈ S] = []"
                  using `?P` by simp
              }
              ultimately show
               "ok_flow_aux_1 c' c'' c' s1 t1 t1 f f'
                  vs1 vs1' vs2 vs1' ws1' ws1' ?cs ∧
                ok_flow_aux_2 s1 s2 t1 t1 f f' vs1 vs1' ?cs ∧
                ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws1' ?cs"
                using L and `?P` by auto
            qed
          qed
        next
          assume "∄S. S ≠ {} ∧
            S ⊆ {x. s1 = t1 (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x)}"
          hence O: "∀c2' t2 vs2' ws2'.
            ok_flow_aux_1 c' c'' c2' s1 t1 t2 f f'
              vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
            ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
            ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
            using L by (auto intro!: ok_flow_aux_degen)
          show ?thesis
            by (rule exI [of _ SKIP], rule exI [of _ "λx. 0"],
             rule exI [of _ "[]"], rule exI [of _ "[]"],
             simp add: O [rule_format, of SKIP "λx. 0" "[]" "[]"])
        qed
      qed (simp add: C [OF _ _ I M N K] G L)
    qed
  next
    assume "bval b s"
    hence J: "s ∈ Univ B1 (⊆ state ∩ X)"
      by (insert btyping2_approx [OF G D], simp)
    assume K: "(c1, s, f, vs0, ws0) →*{tl cfs1} (c', s1, f, vs1, ws1)"
    show ?thesis
      using B [OF _ _ H J K F] and G by simp
  next
    assume "¬ bval b s"
    hence J: "s ∈ Univ B2 (⊆ state ∩ X)"
      by (insert btyping2_approx [OF G D], simp)
    assume K: "(c2, s, f, vs0, ws0) →*{tl cfs1} (c', s1, f, vs1, ws1)"
    show ?thesis
      using C [OF _ _ I J K F] and G by simp
  qed
qed

lemma ctyping2_correct_aux_while:
  assumes
    A: "(U, v) ⊨ WHILE b DO c (⊆ A, X) = Some (B, W)" and
    B: "⋀B1 B2 C Y B1' B2' D Z c1 c2 s s1 s2 vs0 vs1 vs2 ws0 ws1 ws2 cfs1 cfs2.
      (B1, B2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B1, X) ⟹
      (B1', B2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: W ↝ UNIV ⟹
      ({}, False) ⊨ c (⊆ B1, X) = Some (D, Z) ⟹
      s ∈ Univ B1 (⊆ state ∩ X) ⟹
      (c, s, f, vs0, ws0) →*{cfs1} (c1, s1, f, vs1, ws1) ⟹
      (c1, s1, f, vs1, ws1) →*{cfs2} (c2, s2, f, vs2, ws2) ⟹
        ok_flow_aux {} c1 c2 s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)" and
    C: "⋀B1 B2 C Y B1' B2' D' Z' c1 c2 s s1 s2 vs0 vs1 vs2 ws0 ws1 ws2 cfs1 cfs2.
      (B1, B2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B1, X) ⟹
      (B1', B2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: W ↝ UNIV ⟹
      ({}, False) ⊨ c (⊆ B1', Y) = Some (D', Z') ⟹
      s ∈ Univ B1' (⊆ state ∩ Y) ⟹
      (c, s, f, vs0, ws0) →*{cfs1} (c1, s1, f, vs1, ws1) ⟹
      (c1, s1, f, vs1, ws1) →*{cfs2} (c2, s2, f, vs2, ws2) ⟹
        ok_flow_aux {} c1 c2 s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)" and
    D: "s ∈ Univ A (⊆ state ∩ X)" and
    E: "(WHILE b DO c, s, f, vs0, ws0) →*{cfs1} (c1, s1, f, vs1, ws1)" and
    F: "(c1, s1, f, vs1, ws1) →*{cfs2} (c2, s2, f, vs2, ws2)"
 shows "ok_flow_aux U c1 c2 s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)"
proof -
  from A obtain B1 B2 C Y B1' B2' D Z D' Z' where
    G: "⊨ b (⊆ A, X) = (B1, B2)" and
    H: "⊢ c (⊆ B1, X) = (C, Y)" and
    I: "⊨ b (⊆ C, Y) = (B1', B2')" and
    J: "({}, False) ⊨ c (⊆ B1, X) = Some (D, Z)" and
    K: "({}, False) ⊨ c (⊆ B1', Y) = Some (D', Z')" and
    L: "∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U. B: W ↝ UNIV"
    by (fastforce split: if_split_asm option.split_asm prod.split_asm)
  from UnI1 [OF D, of "Univ C (⊆ state ∩ Y)"] and E and F show ?thesis
  proof (induction "cfs1 @ cfs2" arbitrary: cfs1 cfs2 s vs0 ws0 c1 s1 vs1 ws1
   rule: length_induct)
    fix cfs1 cfs2 s vs0 ws0 c1 s1 vs1 ws1
    assume
      M: "∀cfs. length cfs < length (cfs1 @ cfs2) ⟶
        (∀cfs' cfs''. cfs = cfs' @ cfs'' ⟶
          (∀s. s ∈ Univ A (⊆ state ∩ X) ∪ Univ C (⊆ state ∩ Y) ⟶
            (∀vs0 ws0 c1 s1 vs1 ws1.
              (WHILE b DO c, s, f, vs0, ws0) →*{cfs'} (c1, s1, f, vs1, ws1) ⟶
              (c1, s1, f, vs1, ws1) →*{cfs''} (c2, s2, f, vs2, ws2) ⟶
                ok_flow_aux U c1 c2 s1 s2 f vs1 vs2 ws1 ws2 (flow cfs''))))" and
      N: "s ∈ Univ A (⊆ state ∩ X) ∪ Univ C (⊆ state ∩ Y)" and
      O: "(c1, s1, f, vs1, ws1) →*{cfs2} (c2, s2, f, vs2, ws2)"
    assume "(WHILE b DO c, s, f, vs0, ws0) →*{cfs1} (c1, s1, f, vs1, ws1)"
    hence
     "(c1, s1, f, vs1, ws1) = (WHILE b DO c, s, f, vs0, ws0) ∧
        flow cfs1 = [] ∨
      bval b s ∧
        (c;; WHILE b DO c, s, f, vs0, ws0) →*{tl cfs1} (c1, s1, f, vs1, ws1) ∧
        flow cfs1 = ⟨bvars b⟩ # flow (tl cfs1) ∨
      ¬ bval b s ∧
        (c1, s1, f, vs1, ws1) = (SKIP, s, f, vs0, ws0) ∧
        flow cfs1 = [⟨bvars b⟩]"
      by (rule small_stepsl_while)
    thus "ok_flow_aux U c1 c2 s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)"
    proof (rule disjE, erule_tac [2] disjE, erule_tac conjE,
     (erule_tac [2-3] conjE)+)
      assume P: "(c1, s1, f, vs1, ws1) = (WHILE b DO c, s, f, vs0, ws0)"
      hence "(WHILE b DO c, s, f, vs0, ws0) →*{cfs2} (c2, s2, f, vs2, ws2)"
        using O by simp
      hence
       "(c2, s2, f, vs2, ws2) = (WHILE b DO c, s, f, vs0, ws0) ∧
          flow cfs2 = [] ∨
        bval b s ∧
          (c;; WHILE b DO c, s, f, vs0, ws0) →*{tl cfs2}
            (c2, s2, f, vs2, ws2) ∧
          flow cfs2 = ⟨bvars b⟩ # flow (tl cfs2) ∨
        ¬ bval b s ∧
          (c2, s2, f, vs2, ws2) = (SKIP, s, f, vs0, ws0) ∧
          flow cfs2 = [⟨bvars b⟩]"
        by (rule small_stepsl_while)
      thus ?thesis
      proof (rule disjE, erule_tac [2] disjE, erule_tac conjE,
       (erule_tac [2-3] conjE)+)
        assume
         "(c2, s2, f, vs2, ws2) = (WHILE b DO c, s, f, vs0, ws0)" and
         "flow cfs2 = []"
        thus ?thesis
          using P by fastforce
      next
        assume
          Q: "bval b s" and
          R: "flow cfs2 = ⟨bvars b⟩ # flow (tl cfs2)"
            (is "?cs = _ # ?cs'")
        assume "(c;; WHILE b DO c, s, f, vs0, ws0) →*{tl cfs2}
          (c2, s2, f, vs2, ws2)"
        hence
         "(∃c' cfs.
            c2 = c';; WHILE b DO c ∧
            (c, s, f, vs0, ws0) →*{cfs} (c', s2, f, vs2, ws2) ∧
            ?cs' = flow cfs) ∨
          (∃p cfs' cfs''.
            length cfs'' < length (tl cfs2) ∧
            (c, s, f, vs0, ws0) →*{cfs'} (SKIP, p) ∧
            (WHILE b DO c, p) →*{cfs''} (c2, s2, f, vs2, ws2) ∧
            ?cs' = flow cfs' @ flow cfs'')"
          by (rule small_stepsl_seq)
        thus ?thesis
          apply (rule disjE)
           apply (erule exE)+
           apply (erule conjE)+
          subgoal for c' cfs
          proof -
            assume
              S: "c2 = c';; WHILE b DO c" and
              T: "(c, s, f, vs0, ws0) →*{cfs} (c', s2, f, vs2, ws2)" and
              U: "?cs' = flow cfs"
            have V: "(c, s, f, vs0, ws0) →*{[]} (c, s, f, vs0, ws0)"
              by simp
            from N have
             "ok_flow_aux {} c c' s s2 f vs0 vs2 ws0 ws2 (flow cfs)"
            proof
              assume W: "s ∈ Univ A (⊆ state ∩ X)"
              have X: "s ∈ Univ B1 (⊆ state ∩ X)"
                using Q by (insert btyping2_approx [OF G W], simp)
              show ?thesis
                by (rule B [OF G [symmetric] H [symmetric] I [symmetric]
                 L J X V T])
            next
              assume W: "s ∈ Univ C (⊆ state ∩ Y)"
              have X: "s ∈ Univ B1' (⊆ state ∩ Y)"
                using Q by (insert btyping2_approx [OF I W], simp)
              show ?thesis
                by (rule C [OF G [symmetric] H [symmetric] I [symmetric]
                 L K X V T])
            qed
            hence W: "ok_flow_aux {} c c' s1 s2 f vs1 vs2 ws1 ws2 ?cs'"
              using P and U by simp
            show ?thesis
            proof (rule conjI, clarify)
              fix t1 f' vs1' ws1'
              obtain c2' and t2 and vs2' and ws2' where
               "ok_flow_aux_1 c c' c2' s1 t1 t2 f f'
                  vs1 vs1' vs2 vs2' ws1' ws2' ?cs' ∧
                ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs' ∧
                ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs'"
                (is "?P1 ∧ ?P2 ∧ ?P3")
                using W by fastforce
              hence ?P1 and ?P2 and ?P3 by auto
              show "∃c2' t2 vs2' ws2'.
                ok_flow_aux_1 c1 c2 c2' s1 t1 t2 f f'
                  vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
                ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
                ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
              proof (rule exI [of _ "c2';; WHILE b DO c"], rule exI [of _ t2],
               rule exI [of _ vs2'], rule exI [of _ ws2'])
                {
                  fix S
                  assume
                    X: "S ≠ {}" and
                    Y: "S ⊆ {x. s1 = t1
                      (⊆ sources_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x)}" and
                    Z: "f = f' (⊆ vs1, vs1',
                      ⋃ {tags_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x | x. x ∈ S})"
                  have "∀x. sources_aux ?cs' vs1 s1 f x ⊆
                    sources_aux (⟨bvars b⟩ # ?cs') vs1 s1 f x"
                    by (blast intro: subsetD [OF sources_aux_observe_tl])
                  hence "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs' vs1 s1 f x)}"
                    using Y by blast
                  moreover have "f = f' (⊆ vs1, vs1',
                    ⋃ {tags_aux ?cs' vs1 s1 f x | x. x ∈ S})"
                    using Z by (simp add: tags_aux_observe_tl)
                  ultimately have
                   "(c, t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2') ∧
                    map fst [p←drop (length vs1) vs2. fst p ∈ S] =
                      map fst [p←drop (length vs1') vs2'. fst p ∈ S]"
                    (is "?Q1 ∧ ?Q2")
                    using X and `?P1` by simp
                  hence ?Q1 and ?Q2 by auto
                  have "s1 = t1 (⊆ bvars b)"
                    by (rule eq_states_while [OF Y X], insert L N P, simp+)
                  hence "bval b t1"
                    using P and Q by (blast dest: bvars_bval)
                  hence "(WHILE b DO c, t1, f', vs1', ws1') →
                    (c;; WHILE b DO c, t1, f', vs1', ws1')" ..
                  hence "(c1, t1, f', vs1', ws1') →*
                    (c2';; WHILE b DO c, t2, f', vs2', ws2')"
                    using P and `?Q1` by (blast intro: star_seq2 star_trans)
                  hence "?this ∧ ?Q2"
                    using `?Q2` by simp
                }
                moreover {
                  fix S
                  assume
                    X: "S ⊆ {x. s1 = t1
                      (⊆ sources (⟨bvars b⟩ # ?cs') vs1 s1 f x)}" and
                    Y: "f = f' (⊆ vs1, vs1',
                      ⋃ {tags (⟨bvars b⟩ # ?cs') vs1 s1 f x | x. x ∈ S})"
                  have "∀x. sources ?cs' vs1 s1 f x ⊆
                    sources (⟨bvars b⟩ # ?cs') vs1 s1 f x"
                    by (blast intro: subsetD [OF sources_observe_tl])
                  hence "S ⊆ {x. s1 = t1 (⊆ sources ?cs' vs1 s1 f x)}"
                    using X by blast
                  moreover have "f = f' (⊆ vs1, vs1',
                    ⋃ {tags ?cs' vs1 s1 f x | x. x ∈ S})"
                    using Y by (simp add: tags_observe_tl)
                  ultimately have "s2 = t2 (⊆ S)"
                    using `?P2` by blast
                }
                moreover {
                  fix S
                  assume
                    X: "S ≠ {}" and
                    Y: "S ⊆ {x. s1 = t1
                      (⊆ sources_out (⟨bvars b⟩ # ?cs') vs1 s1 f x)}" and
                    Z: "f = f' (⊆ vs1, vs1',
                      ⋃ {tags_out (⟨bvars b⟩ # ?cs') vs1 s1 f x | x. x ∈ S})"
                  have "∀x. sources_out ?cs' vs1 s1 f x ⊆
                    sources_out (⟨bvars b⟩ # ?cs') vs1 s1 f x"
                    by (blast intro: subsetD [OF sources_out_observe_tl])
                  hence "S ⊆ {x. s1 = t1 (⊆ sources_out ?cs' vs1 s1 f x)}"
                    using Y by blast
                  moreover have "f = f' (⊆ vs1, vs1',
                    ⋃ {tags_out ?cs' vs1 s1 f x | x. x ∈ S})"
                    using Z by (simp add: tags_out_observe_tl)
                  ultimately have "[p←drop (length ws1) ws2. fst p ∈ S] =
                    [p←drop (length ws1') ws2'. fst p ∈ S]"
                    using X and `?P3` by simp
                }
                ultimately show
                 "ok_flow_aux_1 c1 c2 (c2';; WHILE b DO c) s1 t1 t2 f f'
                    vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
                  ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
                  ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
                  using R and S by auto
              qed
            qed (insert L, auto simp: no_upd_empty)
          qed
          apply (erule exE)+
          apply (erule conjE)+
          subgoal for p cfs' cfs''
          proof -
            assume "(c, s, f, vs0, ws0) →*{cfs'} (SKIP, p)"
            moreover from this obtain s1' and vs and ws where
              S: "p = (s1', f, vs, ws)"
              by (blast dest: small_stepsl_stream)
            ultimately have
              T: "(c, s1, f, vs1, ws1) →*{cfs'} (SKIP, s1', f, vs, ws)"
              using P by simp
            assume "(WHILE b DO c, p) →*{cfs''} (c2, s2, f, vs2, ws2)"
            with S have
              U: "(WHILE b DO c, s1', f, vs, ws) →*{cfs''}
                (c2, s2, f, vs2, ws2)"
              by simp
            assume V: "?cs' = flow cfs' @ flow cfs''"
              (is "(_ :: flow) = ?cs1' @ ?cs2'")
            have W: "(c, s1, f, vs1, ws1) →*{[]} (c, s1, f, vs1, ws1)"
              by simp
            from N have "ok_flow_aux {} c SKIP s1 s1' f vs1 vs ws1 ws ?cs1'"
            proof
              assume X: "s ∈ Univ A (⊆ state ∩ X)"
              have Y: "s1 ∈ Univ B1 (⊆ state ∩ X)"
                using P and Q by (insert btyping2_approx [OF G X], simp)
              show ?thesis
                by (rule B [OF G [symmetric] H [symmetric] I [symmetric]
                 L J Y W T])
            next
              assume X: "s ∈ Univ C (⊆ state ∩ Y)"
              have Y: "s1 ∈ Univ B1' (⊆ state ∩ Y)"
                using P and Q by (insert btyping2_approx [OF I X], simp)
              show ?thesis
                by (rule C [OF G [symmetric] H [symmetric] I [symmetric]
                 L K Y W T])
            qed
            hence X: "ok_flow_aux {} c SKIP s1 s1' f vs1 vs ws1 ws ?cs1'"
              using P by simp
            assume "length cfs'' < length (tl cfs2)"
            hence "length ([] @ cfs'') < length (cfs1 @ cfs2)"
              by simp
            moreover have "[] @ cfs'' = [] @ cfs''" ..
            moreover from T have "(c, s, f, vs0, ws0) ⇒ (s1', f, vs, ws)"
              using P by (auto dest: small_stepsl_steps simp: big_iff_small)
            hence "s1' ∈ Univ A (⊆ state ∩ X) ∪ Univ C (⊆ state ∩ Y)"
              by (rule univ_states_while [OF _ G H I J K Q N])
            moreover have "(WHILE b DO c, s1', f, vs, ws) →*{[]}
              (WHILE b DO c, s1', f, vs, ws)"
              by simp
            ultimately have
              Y: "ok_flow_aux U (WHILE b DO c) c2 s1' s2 f vs vs2 ws ws2 ?cs2'"
              using U by (rule M [rule_format])
            show ?thesis
            proof (rule conjI, clarify)
              fix t1 f' vs1' ws1'
              obtain c1'' and t1' and vs1'' and ws1'' where
               "ok_flow_aux_1 c SKIP c1'' s1 t1 t1' f f'
                  vs1 vs1' vs vs1'' ws1' ws1'' ?cs1' ∧
                ok_flow_aux_2 s1 s1' t1 t1' f f' vs1 vs1' ?cs1' ∧
                ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws ws1'' ?cs1'"
                (is "_ ∧ ?P2 ∧ ?P3")
                using X by fastforce
              hence
               "ok_flow_aux_1 c SKIP SKIP s1 t1 t1' f f'
                  vs1 vs1' vs vs1'' ws1' ws1'' ?cs1'"
                (is ?P1) and ?P2 and ?P3 by auto
              obtain c2' and t2 and vs2' and ws2' where
               "ok_flow_aux_1 (WHILE b DO c) c2 c2' s1' t1' t2 f f'
                  vs vs1'' vs2 vs2' ws1'' ws2' ?cs2' ∧
                ok_flow_aux_2 s1' s2 t1' t2 f f' vs vs1'' ?cs2' ∧
                ok_flow_aux_3 s1' t1' f f' vs vs1'' ws ws1'' ws2 ws2' ?cs2'"
                (is "?P1' ∧ ?P2' ∧ ?P3'")
                using Y by fastforce
              hence ?P1' and ?P2' and ?P3' by auto
              show "∃c2' t2 vs2' ws2'.
                ok_flow_aux_1 c1 c2 c2' s1 t1 t2 f f'
                  vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
                ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
                ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
              proof (rule exI [of _ c2'], rule exI [of _ t2],
               rule exI [of _ vs2'], rule exI [of _ ws2'])
                {
                  fix S
                  assume
                    Z: "S ≠ {}" and
                    AA: "S ⊆ {x. s1 = t1 (⊆ sources_aux
                      (⟨bvars b⟩ # ?cs1' @ ?cs2') vs1 s1 f x)}" and
                    AB: "f = f' (⊆ vs1, vs1', ⋃ {tags_aux
                      (⟨bvars b⟩ # ?cs1' @ ?cs2') vs1 s1 f x | x. x ∈ S})"
                  have "∀x. sources_aux (?cs1' @ ?cs2') vs1 s1 f x ⊆
                    sources_aux (⟨bvars b⟩ # ?cs1' @ ?cs2') vs1 s1 f x"
                    by (blast intro: subsetD [OF sources_aux_observe_tl])
                  hence AC: "S ⊆ {x. s1 = t1
                    (⊆ sources_aux (?cs1' @ ?cs2') vs1 s1 f x)}"
                    using AA by blast
                  moreover have "∀x. sources_aux ?cs1' vs1 s1 f x ⊆
                    sources_aux (?cs1' @ ?cs2') vs1 s1 f x"
                    by (blast intro: subsetD [OF sources_aux_append])
                  ultimately have
                    AD: "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs1' vs1 s1 f x)}"
                    by blast
                  have AE: "f = f' (⊆ vs1, vs1',
                    ⋃ {tags_aux (?cs1' @ ?cs2') vs1 s1 f x | x. x ∈ S})"
                    (is "_ = _ (⊆ _, _, ?T)")
                    using AB by (simp add: tags_aux_observe_tl)
                  moreover have
                   "⋃ {tags_aux ?cs1' vs1 s1 f x | x. x ∈ S} ⊆ ?T"
                    (is "?T' ⊆ _")
                    by (blast intro: subsetD [OF tags_aux_append])
                  ultimately have "f = f' (⊆ vs1, vs1', ?T')"
                    by (rule eq_streams_subset)
                  hence
                   "(c, t1, f', vs1', ws1') →* (SKIP, t1', f', vs1'', ws1'') ∧
                    map fst [p←drop (length vs1) vs. fst p ∈ S] =
                      map fst [p←drop (length vs1') vs1''. fst p ∈ S]"
                    (is "?Q1 ∧ ?Q2")
                    using Z and AD and `?P1` by simp
                  hence ?Q1 and ?Q2 by auto
                  have "S ⊆ {x. s1' = t1' (⊆ sources_aux ?cs2' vs s1' f x)}"
                    by (rule sources_aux_rhs [OF AC AE T `?P2`])
                  moreover have "f = f' (⊆ vs, vs1'',
                    ⋃ {tags_aux ?cs2' vs s1' f x | x. x ∈ S})"
                    by (rule tags_aux_rhs [OF AC AE T `?Q1` `?P1`])
                  ultimately have
                   "(WHILE b DO c, t1', f', vs1'', ws1'') →*
                      (c2', t2, f', vs2', ws2') ∧
                    (c2 = SKIP) = (c2' = SKIP) ∧
                    map fst [p←drop (length vs) vs2. fst p ∈ S] =
                      map fst [p←drop (length vs1'') vs2'. fst p ∈ S]"
                    (is "?Q1' ∧ ?R2 ∧ ?Q2'")
                    using Z and `?P1'` by simp
                  hence ?Q1' and ?R2 and ?Q2' by auto
                  have "s1 = t1 (⊆ bvars b)"
                    by (rule eq_states_while [OF AA Z], insert L N P, simp+)
                  hence "bval b t1"
                    using P and Q by (blast dest: bvars_bval)
                  hence "(WHILE b DO c, t1, f', vs1', ws1') →
                    (c;; WHILE b DO c, t1, f', vs1', ws1')" ..
                  moreover have "(c;; WHILE b DO c, t1, f', vs1', ws1') →*
                    (c2', t2, f', vs2', ws2')"
                    using `?Q1` and `?Q1'`
                     by (blast intro: star_seq2 star_trans)
                  ultimately have
                   "(c1, t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2')"
                    (is ?R1)
                    using P by (blast intro: star_trans)
                  moreover have
                   "map fst [p←drop (length vs1) vs2. fst p ∈ S] =
                      map fst [p←drop (length vs1') vs2'. fst p ∈ S]"
                    by (rule small_steps_inputs
                     [OF T U `?Q1` `?Q1'` `?Q2` `?Q2'`])
                  ultimately have "?R1 ∧ ?R2 ∧ ?this"
                    using `?R2` by simp
                }
                moreover {
                  fix S
                  assume
                    Z: "S ≠ {}" and
                    AA: "S ⊆ {x. s1 = t1 (⊆ sources
                      (⟨bvars b⟩ # ?cs1' @ ?cs2') vs1 s1 f x)}" and
                    AB: "f = f' (⊆ vs1, vs1', ⋃ {tags
                      (⟨bvars b⟩ # ?cs1' @ ?cs2') vs1 s1 f x | x. x ∈ S})"
                  have "∀x. sources (?cs1' @ ?cs2') vs1 s1 f x ⊆
                    sources (⟨bvars b⟩ # ?cs1' @ ?cs2') vs1 s1 f x"
                    by (blast intro: subsetD [OF sources_observe_tl])
                  hence AC: "S ⊆ {x. s1 = t1
                    (⊆ sources (?cs1' @ ?cs2') vs1 s1 f x)}"
                    using AA by blast
                  have "∀x. sources_aux (?cs1' @ ?cs2') vs1 s1 f x ⊆
                    sources (?cs1' @ ?cs2') vs1 s1 f x"
                    by (blast intro: subsetD [OF sources_aux_sources])
                  moreover have "∀x. sources_aux ?cs1' vs1 s1 f x ⊆
                    sources_aux (?cs1' @ ?cs2') vs1 s1 f x"
                    by (blast intro: subsetD [OF sources_aux_append])
                  ultimately have
                    AD: "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs1' vs1 s1 f x)}"
                    using AC by blast
                  have AE: "f = f' (⊆ vs1, vs1',
                    ⋃ {tags (?cs1' @ ?cs2') vs1 s1 f x | x. x ∈ S})"
                    (is "_ = _ (⊆ _, _, ?T)")
                    using AB by (simp add: tags_observe_tl)
                  have
                   "⋃ {tags_aux (?cs1' @ ?cs2') vs1 s1 f x | x. x ∈ S} ⊆ ?T"
                    (is "?T' ⊆ _")
                    by (blast intro: subsetD [OF tags_aux_tags])
                  moreover have
                   "⋃ {tags_aux ?cs1' vs1 s1 f x | x. x ∈ S} ⊆ ?T'"
                    (is "?T'' ⊆ _")
                    by (blast intro: subsetD [OF tags_aux_append])
                  ultimately have "?T'' ⊆ ?T"
                    by simp
                  with AE have "f = f' (⊆ vs1, vs1', ?T'')"
                    by (rule eq_streams_subset)
                  hence AF: "(c, t1, f', vs1', ws1') →*
                    (SKIP, t1', f', vs1'', ws1'')"
                    using Z and AD and `?P1` by simp
                  have "S ⊆ {x. s1' = t1' (⊆ sources ?cs2' vs s1' f x)}"
                    by (rule sources_rhs [OF AC AE T `?P2`])
                  moreover have "f = f' (⊆ vs, vs1'',
                    ⋃ {tags ?cs2' vs s1' f x | x. x ∈ S})"
                    by (rule tags_rhs [OF AC AE T AF `?P1`])
                  ultimately have "s2 = t2 (⊆ S)"
                    using `?P2'` by blast
                }
                moreover {
                  fix S
                  assume
                    Z: "S ≠ {}" and
                    AA: "S ⊆ {x. s1 = t1 (⊆ sources_out
                      (⟨bvars b⟩ # ?cs1' @ ?cs2') vs1 s1 f x)}" and
                    AB: "f = f' (⊆ vs1, vs1', ⋃ {tags_out
                      (⟨bvars b⟩ # ?cs1' @ ?cs2') vs1 s1 f x | x. x ∈ S})"
                  have "∀x. sources_out (?cs1' @ ?cs2') vs1 s1 f x ⊆
                    sources_out (⟨bvars b⟩ # ?cs1' @ ?cs2') vs1 s1 f x"
                    by (blast intro: subsetD [OF sources_out_observe_tl])
                  hence AC: "S ⊆ {x. s1 = t1
                    (⊆ sources_out (?cs1' @ ?cs2') vs1 s1 f x)}"
                    using AA by blast
                  have AD: "∀x. sources_aux (?cs1' @ ?cs2') vs1 s1 f x ⊆
                    sources_out (?cs1' @ ?cs2') vs1 s1 f x"
                    by (blast intro: subsetD [OF sources_aux_sources_out])
                  moreover have "∀x. sources_aux ?cs1' vs1 s1 f x ⊆
                    sources_aux (?cs1' @ ?cs2') vs1 s1 f x"
                    by (blast intro: subsetD [OF sources_aux_append])
                  ultimately have
                    AE: "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs1' vs1 s1 f x)}"
                    using AC by blast
                  have AF: "f = f' (⊆ vs1, vs1',
                    ⋃ {tags_out (?cs1' @ ?cs2') vs1 s1 f x | x. x ∈ S})"
                    (is "_ = _ (⊆ _, _, ?T)")
                    using AB by (simp add: tags_out_observe_tl)
                  have AG:
                   "⋃ {tags_aux (?cs1' @ ?cs2') vs1 s1 f x | x. x ∈ S} ⊆ ?T"
                    (is "?T' ⊆ _")
                    by (blast intro: subsetD [OF tags_aux_tags_out])
                  moreover have
                   "⋃ {tags_aux ?cs1' vs1 s1 f x | x. x ∈ S} ⊆ ?T'"
                    (is "?T'' ⊆ _")
                    by (blast intro: subsetD [OF tags_aux_append])
                  ultimately have "?T'' ⊆ ?T"
                    by simp
                  with AF have "f = f' (⊆ vs1, vs1', ?T'')"
                    by (rule eq_streams_subset)
                  hence AH: "(c, t1, f', vs1', ws1') →*
                    (SKIP, t1', f', vs1'', ws1'')"
                    using Z and AE and `?P1` by simp
                  have AI: "S ⊆ {x. s1 = t1
                    (⊆ sources_aux (?cs1' @ ?cs2') vs1 s1 f x)}"
                    using AC and AD by blast
                  have AJ: "f = f' (⊆ vs1, vs1', ?T')"
                    using AF and AG by (rule eq_streams_subset)
                  have "S ⊆ {x. s1' = t1' (⊆ sources_aux ?cs2' vs s1' f x)}"
                    by (rule sources_aux_rhs [OF AI AJ T `?P2`])
                  moreover have "f = f' (⊆ vs, vs1'',
                    ⋃ {tags_aux ?cs2' vs s1' f x | x. x ∈ S})"
                    by (rule tags_aux_rhs [OF AI AJ T AH `?P1`])
                  ultimately have AK:
                   "(WHILE b DO c, t1', f', vs1'', ws1'') →*
                      (c2', t2, f', vs2', ws2')"
                    using Z and `?P1'` by simp
                  have "∀x. sources_out ?cs1' vs1 s1 f x ⊆
                    sources_out (?cs1' @ ?cs2') vs1 s1 f x"
                    by (blast intro: subsetD [OF sources_out_append])
                  hence "S ⊆ {x. s1 = t1 (⊆ sources_out ?cs1' vs1 s1 f x)}"
                    using AC by blast
                  moreover have
                   "⋃ {tags_out ?cs1' vs1 s1 f x | x. x ∈ S} ⊆ ?T"
                    (is "?T' ⊆ _")
                    by (blast intro: subsetD [OF tags_out_append])
                  with AF have "f = f' (⊆ vs1, vs1', ?T')"
                    by (rule eq_streams_subset)
                  ultimately have AL:
                   "[p←drop (length ws1) ws. fst p ∈ S] =
                    [p←drop (length ws1') ws1''. fst p ∈ S]"
                    using Z and `?P3` by simp
                  have "S ⊆ {x. s1' = t1' (⊆ sources_out ?cs2' vs s1' f x)}"
                    by (rule sources_out_rhs [OF AC AF T `?P2`])
                  moreover have "f = f' (⊆ vs, vs1'',
                    ⋃ {tags_out ?cs2' vs s1' f x | x. x ∈ S})"
                    by (rule tags_out_rhs [OF AC AF T AH `?P1`])
                  ultimately have "[p←drop (length ws) ws2. fst p ∈ S] =
                    [p←drop (length ws1'') ws2'. fst p ∈ S]"
                    using Z and `?P3'` by simp
                  hence "[p←drop (length ws1) ws2. fst p ∈ S] =
                    [p←drop (length ws1') ws2'. fst p ∈ S]"
                    by (rule small_steps_outputs [OF T U AH AK AL])
                }
                ultimately show
                 "ok_flow_aux_1 c1 c2 c2' s1 t1 t2 f f'
                    vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
                  ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
                  ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
                  using R and V by auto
              qed
            qed (insert L, auto simp: no_upd_empty)
          qed
          done
      next
        assume
          Q: "¬ bval b s" and
          R: "flow cfs2 = [⟨bvars b⟩]"
            (is "?cs = _")
        assume "(c2, s2, f, vs2, ws2) = (SKIP, s, f, vs0, ws0)"
        hence S: "(c2, s2, f, vs2, ws2) = (SKIP, s1, f, vs1, ws1)"
          using P by simp
        show ?thesis
        proof (rule conjI, clarify)
          fix t1 f' vs1' ws1'
          show "∃c2' t2 vs2' ws2'.
            ok_flow_aux_1 c1 c2 c2' s1 t1 t2 f f'
              vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
            ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
            ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
          proof (rule exI [of _ SKIP], rule exI [of _ t1],
           rule exI [of _ vs1'], rule exI [of _ ws1'])
            {
              fix S
              assume
               "S ⊆ {x. s1 = t1 (⊆ sources_aux [⟨bvars b⟩] vs1 s1 f x)}" and
               "S ≠ {}"
              hence "s1 = t1 (⊆ bvars b)"
                by (rule eq_states_while, insert L N P, simp+)
              hence "¬ bval b t1"
                using P and Q by (blast dest: bvars_bval)
              hence "(c1, t1, f', vs1', ws1') →* (SKIP, t1, f', vs1', ws1')"
                using P by simp
            }
            moreover {
              fix S
              assume "S ⊆ {x. s1 = t1 (⊆ sources [⟨bvars b⟩] vs1 s1 f x)}"
              moreover have "∀x. sources [] vs1 s1 f x ⊆
                sources [⟨bvars b⟩] vs1 s1 f x"
                by (blast intro!: sources_observe_tl)
              ultimately have "s1 = t1 (⊆ S)"
                by auto
            }
            ultimately show
             "ok_flow_aux_1 c1 c2 SKIP s1 t1 t1 f f'
                vs1 vs1' vs2 vs1' ws1' ws1' ?cs ∧
              ok_flow_aux_2 s1 s2 t1 t1 f f' vs1 vs1' ?cs ∧
              ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws1' ?cs"
              using R and S by auto
          qed
        qed (insert L, auto simp: no_upd_empty)
      qed
    next
      assume P: "bval b s"
      assume "(c;; WHILE b DO c, s, f, vs0, ws0) →*{tl cfs1}
        (c1, s1, f, vs1, ws1)"
      hence
       "(∃c' cfs.
          c1 = c';; WHILE b DO c ∧
          (c, s, f, vs0, ws0) →*{cfs} (c', s1, f, vs1, ws1) ∧
          flow (tl cfs1) = flow cfs) ∨
        (∃p cfs' cfs''.
          length cfs'' < length (tl cfs1) ∧
          (c, s, f, vs0, ws0) →*{cfs'} (SKIP, p) ∧
          (WHILE b DO c, p) →*{cfs''} (c1, s1, f, vs1, ws1) ∧
          flow (tl cfs1) = flow cfs' @ flow cfs'')"
        by (rule small_stepsl_seq)
      thus ?thesis
        apply (rule disjE)
         apply (erule exE)+
         apply (erule conjE)+
        subgoal for c' cfs
        proof -
          assume
            Q: "(c, s, f, vs0, ws0) →*{cfs} (c', s1, f, vs1, ws1)" and
            R: "c1 = c';; WHILE b DO c"
          hence "(c';; WHILE b DO c, s1, f, vs1, ws1) →*{cfs2}
            (c2, s2, f, vs2, ws2)"
            using O by simp
          hence
           "(∃c'' cfs'.
              c2 = c'';; WHILE b DO c ∧
              (c', s1, f, vs1, ws1) →*{cfs'} (c'', s2, f, vs2, ws2) ∧
              flow cfs2 = flow cfs') ∨
            (∃p cfs' cfs''.
              length cfs'' < length cfs2 ∧
              (c', s1, f, vs1, ws1) →*{cfs'} (SKIP, p) ∧
              (WHILE b DO c, p) →*{cfs''} (c2, s2, f, vs2, ws2) ∧
              flow cfs2 = flow cfs' @ flow cfs'')"
            by (rule small_stepsl_seq)
          thus ?thesis
            apply (rule disjE)
             apply (erule exE)+
             apply (erule conjE)+
            subgoal for c'' cfs'
            proof -
              assume
                S: "c2 = c'';; WHILE b DO c" and
                T: "(c', s1, f, vs1, ws1) →*{cfs'} (c'', s2, f, vs2, ws2)" and
                U: "flow cfs2 = flow cfs'"
                  (is "?cs = ?cs'")
              from N have "ok_flow_aux {} c' c'' s1 s2 f vs1 vs2 ws1 ws2 ?cs'"
              proof
                assume V: "s ∈ Univ A (⊆ state ∩ X)"
                have W: "s ∈ Univ B1 (⊆ state ∩ X)"
                  using P by (insert btyping2_approx [OF G V], simp)
                show ?thesis
                  by (rule B [OF G [symmetric] H [symmetric] I [symmetric]
                   L J W Q T])
              next
                assume V: "s ∈ Univ C (⊆ state ∩ Y)"
                have W: "s ∈ Univ B1' (⊆ state ∩ Y)"
                  using P by (insert btyping2_approx [OF I V], simp)
                show ?thesis
                  by (rule C [OF G [symmetric] H [symmetric] I [symmetric]
                   L K W Q T])
              qed
              hence V: "ok_flow_aux {} c' c'' s1 s2 f vs1 vs2 ws1 ws2 ?cs"
                using U by simp
              show ?thesis
              proof (rule conjI, clarify)
                fix t1 f' vs1' ws1'
                obtain c2' and t2 and vs2' and ws2' where
                 "ok_flow_aux_1 c' c'' c2' s1 t1 t2 f f'
                    vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
                  ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
                  ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
                  (is "?P1 ∧ ?P2 ∧ ?P3")
                  using V by fastforce
                hence ?P1 and ?P2 and ?P3 by auto
                show "∃c2' t2 vs2' ws2'.
                  ok_flow_aux_1 c1 c2 c2' s1 t1 t2 f f'
                    vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
                  ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
                  ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
                proof (rule exI [of _ "c2';; WHILE b DO c"],
                 rule exI [of _ t2], rule exI [of _ vs2'], rule exI [of _ ws2'])
                  {
                    fix S
                    assume "S ≠ {}" and
                     "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs vs1 s1 f x)}" and
                     "f = f' (⊆ vs1, vs1',
                        ⋃ {tags_aux ?cs vs1 s1 f x | x. x ∈ S})"
                    hence
                     "(c1, t1, f', vs1', ws1') →*
                        (c2';; WHILE b DO c, t2, f', vs2', ws2') ∧
                      map fst [p←drop (length vs1) vs2. fst p ∈ S] =
                        map fst [p←drop (length vs1') vs2'. fst p ∈ S]"
                      using R and `?P1` by (blast intro: star_seq2)
                  }
                  thus
                   "ok_flow_aux_1 c1 c2 (c2';; WHILE b DO c) s1 t1 t2 f f'
                      vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
                    ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
                    ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
                    using S and `?P2` and `?P3` by simp
                qed
              qed (insert L, auto simp: no_upd_empty)
            qed
            apply (erule exE)+
            apply (erule conjE)+
            subgoal for p cfs' cfs''
            proof -
              assume "(c', s1, f, vs1, ws1) →*{cfs'} (SKIP, p)"
              moreover from this obtain s1' and vs and ws where
                S: "p = (s1', f, vs, ws)"
                by (blast dest: small_stepsl_stream)
              ultimately have
                T: "(c', s1, f, vs1, ws1) →*{cfs'} (SKIP, s1', f, vs, ws)"
                by simp
              assume "(WHILE b DO c, p) →*{cfs''} (c2, s2, f, vs2, ws2)"
              with S have
                U: "(WHILE b DO c, s1', f, vs, ws) →*{cfs''}
                  (c2, s2, f, vs2, ws2)"
                by simp
              assume V: "flow cfs2 = flow cfs' @ flow cfs''"
                (is "(?cs :: flow) = ?cs1 @ ?cs2")
              from N have
                W: "ok_flow_aux {} c' SKIP s1 s1' f vs1 vs ws1 ws ?cs1"
              proof
                assume X: "s ∈ Univ A (⊆ state ∩ X)"
                have Y: "s ∈ Univ B1 (⊆ state ∩ X)"
                  using P by (insert btyping2_approx [OF G X], simp)
                show ?thesis
                  by (rule B [OF G [symmetric] H [symmetric] I [symmetric]
                   L J Y Q T])
              next
                assume X: "s ∈ Univ C (⊆ state ∩ Y)"
                have Y: "s ∈ Univ B1' (⊆ state ∩ Y)"
                  using P by (insert btyping2_approx [OF I X], simp)
                show ?thesis
                  by (rule C [OF G [symmetric] H [symmetric] I [symmetric]
                   L K Y Q T])
              qed
              assume "length cfs'' < length cfs2"
              hence "length ([] @ cfs'') < length (cfs1 @ cfs2)"
                by simp
              moreover have "[] @ cfs'' = [] @ cfs''" ..
              moreover have
               "(c, s, f, vs0, ws0) →*{cfs @ cfs'} (SKIP, s1', f, vs, ws)"
                using Q and T by (rule small_stepsl_append)
              hence "(c, s, f, vs0, ws0) ⇒ (s1', f, vs, ws)"
                by (auto dest: small_stepsl_steps simp: big_iff_small)
              hence "s1' ∈ Univ A (⊆ state ∩ X) ∪ Univ C (⊆ state ∩ Y)"
                by (rule univ_states_while [OF _ G H I J K P N])
              moreover have "(WHILE b DO c, s1', f, vs, ws) →*{[]}
                (WHILE b DO c, s1', f, vs, ws)"
                by simp
              ultimately have X:
               "ok_flow_aux U (WHILE b DO c) c2 s1' s2 f vs vs2 ws ws2 ?cs2"
                using U by (rule M [rule_format])
              show ?thesis
              proof (rule conjI, clarify)
                fix t1 f' vs1' ws1'
                obtain c1'' and t1' and vs1'' and ws1'' where
                 "ok_flow_aux_1 c' SKIP c1'' s1 t1 t1' f f'
                    vs1 vs1' vs vs1'' ws1' ws1'' ?cs1 ∧
                  ok_flow_aux_2 s1 s1' t1 t1' f f' vs1 vs1' ?cs1 ∧
                  ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws ws1'' ?cs1"
                  (is "_ ∧ ?P2 ∧ ?P3")
                  using W by fastforce
                hence
                 "ok_flow_aux_1 c' SKIP SKIP s1 t1 t1' f f'
                    vs1 vs1' vs vs1'' ws1' ws1'' ?cs1"
                  (is ?P1) and ?P2 and ?P3 by auto
                obtain c2' and t2 and vs2' and ws2' where
                 "ok_flow_aux_1 (WHILE b DO c) c2 c2' s1' t1' t2 f f'
                    vs vs1'' vs2 vs2' ws1'' ws2' ?cs2 ∧
                  ok_flow_aux_2 s1' s2 t1' t2 f f' vs vs1'' ?cs2 ∧
                  ok_flow_aux_3 s1' t1' f f' vs vs1'' ws ws1'' ws2 ws2' ?cs2"
                  (is "?P1' ∧ ?P2' ∧ ?P3'")
                  using X by fastforce
                hence ?P1' and ?P2' and ?P3' by auto
                show "∃c2' t2 vs2' ws2'.
                  ok_flow_aux_1 c1 c2 c2' s1 t1 t2 f f'
                    vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
                  ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
                  ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
                proof (rule exI [of _ c2'], rule exI [of _ t2],
                 rule exI [of _ vs2'], rule exI [of _ ws2'])
                  {
                    fix S
                    assume
                      Y: "S ≠ {}" and
                      Z: "S ⊆ {x. s1 = t1
                        (⊆ sources_aux (?cs1 @ ?cs2) vs1 s1 f x)}" and
                      AA: "f = f' (⊆ vs1, vs1',
                        ⋃ {tags_aux (?cs1 @ ?cs2) vs1 s1 f x | x. x ∈ S})"
                        (is "_ = _ (⊆ _, _, ?T)")
                    have "∀x. sources_aux ?cs1 vs1 s1 f x ⊆
                      sources_aux (?cs1 @ ?cs2) vs1 s1 f x"
                      by (blast intro: subsetD [OF sources_aux_append])
                    hence "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs1 vs1 s1 f x)}"
                      using Z by blast
                    moreover have
                     "⋃ {tags_aux ?cs1 vs1 s1 f x | x. x ∈ S} ⊆ ?T"
                      (is "?T' ⊆ _")
                      by (blast intro: subsetD [OF tags_aux_append])
                    with AA have "f = f' (⊆ vs1, vs1', ?T')"
                      by (rule eq_streams_subset)
                    ultimately have
                     "(c', t1, f', vs1', ws1') →*
                        (SKIP, t1', f', vs1'', ws1'') ∧
                      map fst [p←drop (length vs1) vs. fst p ∈ S] =
                        map fst [p←drop (length vs1') vs1''. fst p ∈ S]"
                      (is "?Q1 ∧ ?Q2")
                      using Y and `?P1` by simp
                    hence ?Q1 and ?Q2 by auto
                    have "S ⊆ {x. s1' = t1' (⊆ sources_aux ?cs2 vs s1' f x)}"
                      by (rule sources_aux_rhs [OF Z AA T `?P2`])
                    moreover have "f = f' (⊆ vs, vs1'',
                      ⋃ {tags_aux ?cs2 vs s1' f x | x. x ∈ S})"
                      by (rule tags_aux_rhs [OF Z AA T `?Q1` `?P1`])
                    ultimately have
                     "(WHILE b DO c, t1', f', vs1'', ws1'') →*
                        (c2', t2, f', vs2', ws2') ∧
                      (c2 = SKIP) = (c2' = SKIP) ∧
                      map fst [p←drop (length vs) vs2. fst p ∈ S] =
                        map fst [p←drop (length vs1'') vs2'. fst p ∈ S]"
                      (is "?Q1' ∧ ?R2 ∧ ?Q2'")
                      using Y and `?P1'` by simp
                    hence ?Q1' and ?R2 and ?Q2' by auto
                    from R and `?Q1` and `?Q1'` have
                     "(c1, t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2')"
                      (is ?R1)
                      by (blast intro: star_seq2 star_trans)
                    moreover have
                     "map fst [p←drop (length vs1) vs2. fst p ∈ S] =
                        map fst [p←drop (length vs1') vs2'. fst p ∈ S]"
                      by (rule small_steps_inputs
                       [OF T U `?Q1` `?Q1'` `?Q2` `?Q2'`])
                    ultimately have "?R1 ∧ ?R2 ∧ ?this"
                      using `?R2` by simp
                  }
                  moreover {
                    fix S
                    assume
                      Y: "S ≠ {}" and
                      Z: "S ⊆ {x. s1 = t1
                        (⊆ sources (?cs1 @ ?cs2) vs1 s1 f x)}" and
                      AA: "f = f' (⊆ vs1, vs1',
                        ⋃ {tags (?cs1 @ ?cs2) vs1 s1 f x | x. x ∈ S})"
                        (is "_ = _ (⊆ _, _, ?T)")
                    have "∀x. sources_aux (?cs1 @ ?cs2) vs1 s1 f x ⊆
                      sources (?cs1 @ ?cs2) vs1 s1 f x"
                      by (blast intro: subsetD [OF sources_aux_sources])
                    moreover have "∀x. sources_aux ?cs1 vs1 s1 f x ⊆
                      sources_aux (?cs1 @ ?cs2) vs1 s1 f x"
                      by (blast intro: subsetD [OF sources_aux_append])
                    ultimately have
                      AB: "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs1 vs1 s1 f x)}"
                      using Z by blast
                    have
                     "⋃ {tags_aux (?cs1 @ ?cs2) vs1 s1 f x | x. x ∈ S} ⊆ ?T"
                      (is "?T' ⊆ _")
                      by (blast intro: subsetD [OF tags_aux_tags])
                    moreover have
                     "⋃ {tags_aux ?cs1 vs1 s1 f x | x. x ∈ S} ⊆ ?T'"
                      (is "?T'' ⊆ _")
                      by (blast intro: subsetD [OF tags_aux_append])
                    ultimately have "?T'' ⊆ ?T"
                      by simp
                    with AA have "f = f' (⊆ vs1, vs1', ?T'')"
                      by (rule eq_streams_subset)
                    hence AC: "(c', t1, f', vs1', ws1') →*
                      (SKIP, t1', f', vs1'', ws1'')"
                      using Y and AB and `?P1` by simp
                    have "S ⊆ {x. s1' = t1' (⊆ sources ?cs2 vs s1' f x)}"
                      by (rule sources_rhs [OF Z AA T `?P2`])
                    moreover have "f = f' (⊆ vs, vs1'',
                      ⋃ {tags ?cs2 vs s1' f x | x. x ∈ S})"
                      by (rule tags_rhs [OF Z AA T AC `?P1`])
                    ultimately have "s2 = t2 (⊆ S)"
                      using `?P2'` by blast
                  }
                  moreover {
                    fix S
                    assume
                      Y: "S ≠ {}" and
                      Z: "S ⊆ {x. s1 = t1
                        (⊆ sources_out (?cs1 @ ?cs2) vs1 s1 f x)}" and
                      AA: "f = f' (⊆ vs1, vs1',
                        ⋃ {tags_out (?cs1 @ ?cs2) vs1 s1 f x | x. x ∈ S})"
                        (is "_ = _ (⊆ _, _, ?T)")
                    have AB: "∀x. sources_aux (?cs1 @ ?cs2) vs1 s1 f x ⊆
                      sources_out (?cs1 @ ?cs2) vs1 s1 f x"
                      by (blast intro: subsetD [OF sources_aux_sources_out])
                    moreover have "∀x. sources_aux ?cs1 vs1 s1 f x ⊆
                      sources_aux (?cs1 @ ?cs2) vs1 s1 f x"
                      by (blast intro: subsetD [OF sources_aux_append])
                    ultimately have
                      AC: "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs1 vs1 s1 f x)}"
                      using Z by blast
                    have AD:
                     "⋃ {tags_aux (?cs1 @ ?cs2) vs1 s1 f x | x. x ∈ S} ⊆ ?T"
                      (is "?T' ⊆ _")
                      by (blast intro: subsetD [OF tags_aux_tags_out])
                    moreover have
                     "⋃ {tags_aux ?cs1 vs1 s1 f x | x. x ∈ S} ⊆ ?T'"
                      (is "?T'' ⊆ _")
                      by (blast intro: subsetD [OF tags_aux_append])
                    ultimately have "?T'' ⊆ ?T"
                      by simp
                    with AA have "f = f' (⊆ vs1, vs1', ?T'')"
                      by (rule eq_streams_subset)
                    hence AE: "(c', t1, f', vs1', ws1') →*
                      (SKIP, t1', f', vs1'', ws1'')"
                      using Y and AC and `?P1` by simp
                    have AF: "S ⊆ {x. s1 = t1
                      (⊆ sources_aux (?cs1 @ ?cs2) vs1 s1 f x)}"
                      using Z and AB by blast
                    have AG: "f = f' (⊆ vs1, vs1', ?T')"
                      using AA and AD by (rule eq_streams_subset)
                    have "S ⊆ {x. s1' = t1' (⊆ sources_aux ?cs2 vs s1' f x)}"
                      by (rule sources_aux_rhs [OF AF AG T `?P2`])
                    moreover have "f = f' (⊆ vs, vs1'',
                      ⋃ {tags_aux ?cs2 vs s1' f x | x. x ∈ S})"
                      by (rule tags_aux_rhs [OF AF AG T AE `?P1`])
                    ultimately have
                      AH: "(WHILE b DO c, t1', f', vs1'', ws1'') →*
                        (c2', t2, f', vs2', ws2')"
                      using Y and `?P1'` by simp
                    have "∀x. sources_out ?cs1 vs1 s1 f x ⊆
                      sources_out (?cs1 @ ?cs2) vs1 s1 f x"
                      by (blast intro: subsetD [OF sources_out_append])
                    hence "S ⊆ {x. s1 = t1 (⊆ sources_out ?cs1 vs1 s1 f x)}"
                      using Z by blast
                    moreover have
                     "⋃ {tags_out ?cs1 vs1 s1 f x | x. x ∈ S} ⊆ ?T"
                      (is "?T' ⊆ _")
                      by (blast intro: subsetD [OF tags_out_append])
                    with AA have "f = f' (⊆ vs1, vs1', ?T')"
                      by (rule eq_streams_subset)
                    ultimately have AI:
                     "[p←drop (length ws1) ws. fst p ∈ S] =
                      [p←drop (length ws1') ws1''. fst p ∈ S]"
                      using Y and `?P3` by simp
                    have "S ⊆ {x. s1' = t1' (⊆ sources_out ?cs2 vs s1' f x)}"
                      by (rule sources_out_rhs [OF Z AA T `?P2`])
                    moreover have "f = f' (⊆ vs, vs1'',
                      ⋃ {tags_out ?cs2 vs s1' f x | x. x ∈ S})"
                      by (rule tags_out_rhs [OF Z AA T AE `?P1`])
                    ultimately have "[p←drop (length ws) ws2. fst p ∈ S] =
                      [p←drop (length ws1'') ws2'. fst p ∈ S]"
                      using Y and `?P3'` by simp
                    hence "[p←drop (length ws1) ws2. fst p ∈ S] =
                      [p←drop (length ws1') ws2'. fst p ∈ S]"
                      by (rule small_steps_outputs [OF T U AE AH AI])
                  }
                  ultimately show
                   "ok_flow_aux_1 c1 c2 c2' s1 t1 t2 f f'
                      vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
                    ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
                    ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
                    using V by auto
                qed
              qed (insert L, auto simp: no_upd_empty)
            qed
            done
        qed
        apply (erule exE)+
        apply (erule conjE)+
        subgoal for p cfs' cfs''
        proof -
          assume "(c, s, f, vs0, ws0) →*{cfs'} (SKIP, p)"
          moreover from this obtain s1' and vs and ws where
            Q: "p = (s1', f, vs, ws)"
            by (blast dest: small_stepsl_stream)
          ultimately have
            R: "(c, s, f, vs0, ws0) →*{cfs'} (SKIP, s1', f, vs, ws)"
            by simp
          assume "(WHILE b DO c, p) →*{cfs''} (c1, s1, f, vs1, ws1)"
          with Q have S:
           "(WHILE b DO c, s1', f, vs, ws) →*{cfs''} (c1, s1, f, vs1, ws1)"
            by simp
          assume "length cfs'' < length (tl cfs1)"
          hence "length (cfs'' @ cfs2) < length (cfs1 @ cfs2)"
            by simp
          moreover have "cfs'' @ cfs2 = cfs'' @ cfs2" ..
          moreover have "(c, s, f, vs0, ws0) ⇒ (s1', f, vs, ws)"
            using R by (auto dest: small_stepsl_steps simp: big_iff_small)
          hence "s1' ∈ Univ A (⊆ state ∩ X) ∪ Univ C (⊆ state ∩ Y)"
            by (rule univ_states_while [OF _ G H I J K P N])
          ultimately show ?thesis
            using S and O by (rule M [rule_format])
        qed
        done
    next
      assume "(c1, s1, f, vs1, ws1) = (SKIP, s, f, vs0, ws0)"
      moreover from this have
       "(c2, s2, f, vs2, ws2) = (SKIP, s1, f, vs1, ws1) ∧ flow cfs2 = []"
        using O by (blast intro!: small_stepsl_skip)
      ultimately show ?thesis
        by (insert L, fastforce)
    qed
  qed
qed

lemma ctyping2_correct_aux:
 "⟦(U, v) ⊨ c (⊆ A, X) = Some (B, Y); s ∈ Univ A (⊆ state ∩ X);
    (c, s, f, vs0, ws0) →*{cfs1} (c1, s1, f, vs1, ws1);
    (c1, s1, f, vs1, ws1) →*{cfs2} (c2, s2, f, vs2, ws2)⟧ ⟹
  ok_flow_aux U c1 c2 s1 s2 f vs1 vs2 ws1 ws2 (flow cfs2)"
  apply (induction "(U, v)" c A X arbitrary: B Y U v c1 c2 s s1 s2
   vs0 vs1 vs2 ws0 ws1 ws2 cfs1 cfs2 rule: ctyping2.induct)
         apply fastforce
        apply (erule ctyping2_correct_aux_assign, assumption+)
       apply (erule ctyping2_correct_aux_input, assumption+)
      apply (erule ctyping2_correct_aux_output, assumption+)
     apply (erule ctyping2_correct_aux_seq, assumption+)
    apply (erule ctyping2_correct_aux_or, assumption+)
   apply (erule ctyping2_correct_aux_if, assumption+)
  apply (erule ctyping2_correct_aux_while, assumption+)
  done


theorem ctyping2_correct:
  assumes A: "(U, v) ⊨ c (⊆ A, X) = Some (B, Y)"
  shows "correct c A X"
proof (subst correct_def, clarify)
  fix s t c1 c2 s1 s2 f vs vs1 vs2 ws ws1 ws2 cfs2 t1 f' vs1' ws1'
  let ?cs = "flow cfs2"
  assume "t ∈ A" and "s = t (⊆ state ∩ X)"
  hence "s ∈ Univ A (⊆ state ∩ X)"
    by blast
  moreover assume "(c, s, f, vs, ws) →* (c1, s1, f, vs1, ws1)"
  then obtain cfs1 where "(c, s, f, vs, ws) →*{cfs1} (c1, s1, f, vs1, ws1)"
    by (blast dest: small_steps_stepsl)
  moreover assume "(c1, s1, f, vs1, ws1) →*{cfs2} (c2, s2, f, vs2, ws2)"
  ultimately have "ok_flow_aux U c1 c2 s1 s2 f vs1 vs2 ws1 ws2 ?cs"
    by (rule ctyping2_correct_aux [OF A])
  then obtain c2' and t2 and vs2' and ws2' where
   "ok_flow_aux_1 c1 c2 c2' s1 t1 t2 f f' vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
    ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' ?cs ∧
    ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' ?cs"
    (is "?P1 ∧ ?P2 ∧ ?P3")
    by fastforce
  hence ?P1 and ?P2 and ?P3 by auto
  show "∃c2' t2 vs2' ws2'.
    ok_flow_1 c1 c2 c2' s1 s2 t1 t2 f f' vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
    ok_flow_2 c1 c2 c2' s1 t1 t2 f f' vs1 vs1' vs2 vs2' ws1 ws1' ws2 ws2' ?cs"
  proof (rule exI [of _ c2'], rule exI [of _ t2],
   rule exI [of _ vs2'], rule exI [of _ ws2'])
    {
      fix S
      assume
        B: "S ≠ {}" and
        C: "S ⊆ {x. s1 = t1 (⊆ sources ?cs vs1 s1 f x)}" and
        D: "f = f' (⊆ vs1, vs1', ⋃ {tags ?cs vs1 s1 f x | x. x ∈ S})"
          (is "_ = _ (⊆ _, _, ?T)")
      have "∀x. sources_aux ?cs vs1 s1 f x ⊆ sources ?cs vs1 s1 f x"
        by (blast intro: subsetD [OF sources_aux_sources])
      hence "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs vs1 s1 f x)}"
        using C by blast
      moreover have "⋃ {tags_aux ?cs vs1 s1 f x | x. x ∈ S} ⊆ ?T"
        (is "?T' ⊆ _")
        by (blast intro: subsetD [OF tags_aux_tags])
      with D have "f = f' (⊆ vs1, vs1', ?T')"
        by (rule eq_streams_subset)
      ultimately have
       "(c1, t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2') ∧
        (c2 = SKIP) = (c2' = SKIP) ∧
        map fst [p←drop (length vs1) vs2. fst p ∈ S] =
          map fst [p←drop (length vs1') vs2'. fst p ∈ S]"
        (is ?Q)
        using B and `?P1` by simp
      moreover have "s2 = t2 (⊆ S)"
        using B and C and D and `?P2` by simp
      ultimately have "?Q ∧ ?this" ..
    }
    moreover {
      fix S
      assume
        B: "S ≠ {}" and
        C: "S ⊆ {x. s1 = t1 (⊆ sources_out ?cs vs1 s1 f x)}" and
        D: "f = f' (⊆ vs1, vs1', ⋃ {tags_out ?cs vs1 s1 f x | x. x ∈ S})"
          (is "_ = _ (⊆ _, _, ?T)")
      have "∀x. sources_aux ?cs vs1 s1 f x ⊆ sources_out ?cs vs1 s1 f x"
        by (blast intro: subsetD [OF sources_aux_sources_out])
      hence "S ⊆ {x. s1 = t1 (⊆ sources_aux ?cs vs1 s1 f x)}"
        using C by blast
      moreover have "⋃ {tags_aux ?cs vs1 s1 f x | x. x ∈ S} ⊆ ?T"
        (is "?T' ⊆ _")
        by (blast intro: subsetD [OF tags_aux_tags_out])
      with D have "f = f' (⊆ vs1, vs1', ?T')"
        by (rule eq_streams_subset)
      ultimately have
       "(c1, t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2') ∧
        (c2 = SKIP) = (c2' = SKIP) ∧
        map fst [p←drop (length vs1) vs2. fst p ∈ S] =
          map fst [p←drop (length vs1') vs2'. fst p ∈ S]"
        (is ?Q)
        using B and `?P1` by simp
      moreover have
       "[p←drop (length ws1) ws2. fst p ∈ S] =
          [p←drop (length ws1') ws2'. fst p ∈ S]"
        using B and C and D and `?P3` by simp
      ultimately have "?Q ∧ ?this" ..
    }
    ultimately show
     "ok_flow_1 c1 c2 c2' s1 s2 t1 t2 f f' vs1 vs1' vs2 vs2' ws1' ws2' ?cs ∧
      ok_flow_2 c1 c2 c2' s1 t1 t2 f f' vs1 vs1' vs2 vs2' ws1 ws1' ws2 ws2' ?cs"
      by auto
  qed
qed

end

end