# Theory Mul_Gar_Coll

Up to index of Isabelle/HOL/HoareParallel

theory Mul_Gar_Coll
imports Graph OG_Syntax
begin

    header {* \section{The Multi-Mutator Case} *}

    theory Mul_Gar_Coll imports Graph OG_Syntax begin

    text {*  The full theory takes aprox. 18 minutes.  *}

    record mut =
      Z :: bool
      R :: nat
      T :: nat

    text {* Declaration of variables: *}

    record mul_gar_coll_state =
      M :: nodes
      E :: edges
      bc :: "nat set"
      obc :: "nat set"
      Ma :: nodes
      ind :: nat
      k :: nat
      q :: nat
      l :: nat
      Muts :: "mut list"

    subsection {* The Mutators *}

    constdefs
      Mul_mut_init :: "mul_gar_coll_state => nat => bool"
      "Mul_mut_init ≡ « λn. n=length ´Muts ∧ (∀i<n. R (´Muts!i)<length ´E
                              ∧ T (´Muts!i)<length ´M) »"

      Mul_Redirect_Edge  :: "nat => nat => mul_gar_coll_state ann_com"
      "Mul_Redirect_Edge j n ≡
      .{´Mul_mut_init n ∧ Z (´Muts!j)}.
      ⟨IF T(´Muts!j) ∈ Reach ´E THEN
      ´E:= ´E[R (´Muts!j):= (fst (´E!R(´Muts!j)), T (´Muts!j))] FI,,
      ´Muts:= ´Muts[j:= (´Muts!j) (|Z:=False|)),]⟩"

      Mul_Color_Target :: "nat => nat => mul_gar_coll_state ann_com"
      "Mul_Color_Target j n ≡
      .{´Mul_mut_init n ∧ ¬ Z (´Muts!j)}.
      ⟨´M:=´M[T (´Muts!j):=Black],, ´Muts:=´Muts[j:= (´Muts!j) (|Z:=True|)),]⟩"

      Mul_Mutator :: "nat => nat =>  mul_gar_coll_state ann_com"
      "Mul_Mutator j n ≡
      .{´Mul_mut_init n ∧ Z (´Muts!j)}.
      WHILE True
        INV .{´Mul_mut_init n ∧ Z (´Muts!j)}.
      DO Mul_Redirect_Edge j n ;;
         Mul_Color_Target j n
      OD"

    lemmas mul_mutator_defs = Mul_mut_init_def Mul_Redirect_Edge_def Mul_Color_Target_def

    subsubsection {* Correctness of the proof outline of one mutator *}

    lemma Mul_Redirect_Edge: "0≤j ∧ j<n ==>
      \<turnstile> Mul_Redirect_Edge j n
         pre(Mul_Color_Target j n)"
    apply (unfold mul_mutator_defs)
    apply annhoare
    apply(simp_all)
    apply clarify
    apply(simp add:nth_list_update)
    done

    lemma Mul_Color_Target: "0≤j ∧ j<n ==>
      \<turnstile>  Mul_Color_Target j n
        .{´Mul_mut_init n ∧ Z (´Muts!j)}."
    apply (unfold mul_mutator_defs)
    apply annhoare
    apply(simp_all)
    apply clarify
    apply(simp add:nth_list_update)
    done

    lemma Mul_Mutator: "0≤j ∧ j<n ==>
     \<turnstile> Mul_Mutator j n .{False}."
    apply(unfold Mul_Mutator_def)
    apply annhoare
    apply(simp_all add:Mul_Redirect_Edge Mul_Color_Target)
    apply(simp add:mul_mutator_defs Mul_Redirect_Edge_def)
    done

    subsubsection {* Interference freedom between mutators *}

    lemma Mul_interfree_Redirect_Edge_Redirect_Edge:
      "[|0≤i; i<n; 0≤j; j<n; i≠j|] ==>
      interfree_aux (Some (Mul_Redirect_Edge i n),{}, Some(Mul_Redirect_Edge j n))"
    apply (unfold mul_mutator_defs)
    apply interfree_aux
    apply safe
    apply(simp_all add: nth_list_update)
    done

    lemma Mul_interfree_Redirect_Edge_Color_Target:
      "[|0≤i; i<n; 0≤j; j<n; i≠j|] ==>
      interfree_aux (Some(Mul_Redirect_Edge i n),{},Some(Mul_Color_Target j n))"
    apply (unfold mul_mutator_defs)
    apply interfree_aux
    apply safe
    apply(simp_all add: nth_list_update)
    done

    lemma Mul_interfree_Color_Target_Redirect_Edge:
      "[|0≤i; i<n; 0≤j; j<n; i≠j|] ==>
      interfree_aux (Some(Mul_Color_Target i n),{},Some(Mul_Redirect_Edge j n))"
    apply (unfold mul_mutator_defs)
    apply interfree_aux
    apply safe
    apply(simp_all add:nth_list_update)
    done

    lemma Mul_interfree_Color_Target_Color_Target:
      " [|0≤i; i<n; 0≤j; j<n; i≠j|] ==>
      interfree_aux (Some(Mul_Color_Target i n),{},Some(Mul_Color_Target j n))"
    apply (unfold mul_mutator_defs)
    apply interfree_aux
    apply safe
    apply(simp_all add: nth_list_update)
    done

    lemmas mul_mutator_interfree =
      Mul_interfree_Redirect_Edge_Redirect_Edge Mul_interfree_Redirect_Edge_Color_Target
      Mul_interfree_Color_Target_Redirect_Edge Mul_interfree_Color_Target_Color_Target

    lemma Mul_interfree_Mutator_Mutator: "[|i < n; j < n; i ≠ j|] ==>
      interfree_aux (Some (Mul_Mutator i n), {}, Some (Mul_Mutator j n))"
    apply(unfold Mul_Mutator_def)
    apply(interfree_aux)
    apply(simp_all add:mul_mutator_interfree)
    apply(simp_all add: mul_mutator_defs)
    apply(tactic {* TRYALL (interfree_aux_tac) *})
    apply(tactic {* ALLGOALS Clarify_tac *})
    apply (simp_all add:nth_list_update)
    done

    subsubsection {* Modular Parameterized Mutators *}

    lemma Mul_Parameterized_Mutators: "0<n ==>
     \<parallel>- .{´Mul_mut_init n ∧ (∀i<n. Z (´Muts!i))}.
     COBEGIN
     SCHEME  [0≤ j< n]
      Mul_Mutator j n
     .{False}.
     COEND
     .{False}."
    apply oghoare
    apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update)
    apply(erule Mul_Mutator)
    apply(simp add:Mul_interfree_Mutator_Mutator)
    apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update)
    done

    subsection {* The Collector *}

    constdefs
      Queue :: "mul_gar_coll_state => nat"
     "Queue ≡ « length (filter (λi. ¬ Z i ∧ ´M!(T i) ≠ Black) ´Muts) »"

    consts  M_init :: nodes

    constdefs
      Proper_M_init :: "mul_gar_coll_state => bool"
      "Proper_M_init ≡ « Blacks M_init=Roots ∧ length M_init=length ´M »"

      Mul_Proper :: "mul_gar_coll_state => nat => bool"
      "Mul_Proper ≡ « λn. Proper_Roots ´M ∧ Proper_Edges (´M, ´E) ∧ ´Proper_M_init ∧ n=length ´Muts »"

      Safe :: "mul_gar_coll_state => bool"
      "Safe ≡ « Reach ´E ⊆ Blacks ´M »"

    lemmas mul_collector_defs = Proper_M_init_def Mul_Proper_def Safe_def

    subsubsection {* Blackening Roots *}

    constdefs
      Mul_Blacken_Roots :: "nat =>  mul_gar_coll_state ann_com"
      "Mul_Blacken_Roots n ≡
      .{´Mul_Proper n}.
      ´ind:=0;;
      .{´Mul_Proper n ∧ ´ind=0}.
      WHILE ´ind<length ´M
        INV .{´Mul_Proper n ∧ (∀i<´ind. i∈Roots --> ´M!i=Black) ∧ ´ind≤length ´M}.
      DO .{´Mul_Proper n ∧ (∀i<´ind. i∈Roots --> ´M!i=Black) ∧ ´ind<length ´M}.
           IF ´ind∈Roots THEN
         .{´Mul_Proper n ∧ (∀i<´ind. i∈Roots --> ´M!i=Black) ∧ ´ind<length ´M ∧ ´ind∈Roots}.
           ´M:=´M[´ind:=Black] FI;;
         .{´Mul_Proper n ∧ (∀i<´ind+1. i∈Roots --> ´M!i=Black) ∧ ´ind<length ´M}.
           ´ind:=´ind+1
      OD"

    lemma Mul_Blacken_Roots:
      "\<turnstile> Mul_Blacken_Roots n
      .{´Mul_Proper n ∧ Roots ⊆ Blacks ´M}."
    apply (unfold Mul_Blacken_Roots_def)
    apply annhoare
    apply(simp_all add:mul_collector_defs Graph_defs)
    apply safe
    apply(simp_all add:nth_list_update)
      apply (erule less_SucE)
       apply simp+
     apply force
    apply force
    done

    subsubsection {* Propagating Black *}

    constdefs
      Mul_PBInv :: "mul_gar_coll_state => bool"
      "Mul_PBInv ≡  «´Safe ∨ ´obc⊂Blacks ´M ∨ ´l<´Queue
                     ∨ (∀i<´ind. ¬BtoW(´E!i,´M)) ∧ ´l≤´Queue»"

      Mul_Auxk :: "mul_gar_coll_state => bool"
      "Mul_Auxk ≡ «´l<´Queue ∨ ´M!´k≠Black ∨ ¬BtoW(´E!´ind, ´M) ∨ ´obc⊂Blacks ´M»"

    constdefs
      Mul_Propagate_Black :: "nat =>  mul_gar_coll_state ann_com"
      "Mul_Propagate_Black n ≡
     .{´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M
      ∧ (´Safe ∨ ´l≤´Queue ∨ ´obc⊂Blacks ´M)}.
     ´ind:=0;;
     .{´Mul_Proper n ∧ Roots⊆Blacks ´M
       ∧ ´obc⊆Blacks ´M ∧ Blacks ´M⊆Blacks ´M ∧ ´bc⊆Blacks ´M
       ∧ (´Safe ∨ ´l≤´Queue ∨ ´obc⊂Blacks ´M) ∧ ´ind=0}.
     WHILE ´ind<length ´E
      INV .{´Mul_Proper n ∧ Roots⊆Blacks ´M
            ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M
            ∧ ´Mul_PBInv ∧ ´ind≤length ´E}.
     DO .{´Mul_Proper n ∧ Roots⊆Blacks ´M
         ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M
         ∧ ´Mul_PBInv ∧ ´ind<length ´E}.
       IF ´M!(fst (´E!´ind))=Black THEN
       .{´Mul_Proper n ∧ Roots⊆Blacks ´M
         ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M
         ∧ ´Mul_PBInv ∧ (´M!fst(´E!´ind))=Black ∧ ´ind<length ´E}.
        ´k:=snd(´E!´ind);;
       .{´Mul_Proper n ∧ Roots⊆Blacks ´M
         ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M
         ∧ (´Safe ∨ ´obc⊂Blacks ´M ∨ ´l<´Queue ∨ (∀i<´ind. ¬BtoW(´E!i,´M))
            ∧ ´l≤´Queue ∧ ´Mul_Auxk ) ∧ ´k<length ´M ∧ ´M!fst(´E!´ind)=Black
         ∧ ´ind<length ´E}.
       ⟨´M:=´M[´k:=Black],,´ind:=´ind+1⟩
       ELSE .{´Mul_Proper n ∧ Roots⊆Blacks ´M
             ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M
             ∧ ´Mul_PBInv ∧ ´ind<length ´E}.
             ⟨IF ´M!(fst (´E!´ind))≠Black THEN ´ind:=´ind+1 FI⟩ FI
     OD"

    lemma Mul_Propagate_Black:
      "\<turnstile> Mul_Propagate_Black n
       .{´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M
         ∧ (´Safe ∨ ´obc⊂Blacks ´M ∨ ´l<´Queue ∧ (´l≤´Queue ∨ ´obc⊂Blacks ´M))}."
    apply(unfold Mul_Propagate_Black_def)
    apply annhoare
    apply(simp_all add:Mul_PBInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def)
    --{* 8 subgoals left *}
    apply force
    apply force
    apply force
    apply(force simp add:BtoW_def Graph_defs)
    --{* 4 subgoals left *}
    apply clarify
    apply(simp add: mul_collector_defs Graph12 Graph6 Graph7 Graph8)
    apply(disjE_tac)
     apply(simp_all add:Graph12 Graph13)
     apply(case_tac "M x! k x=Black")
      apply(simp add: Graph10)
     apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
    apply(case_tac "M x! k x=Black")
     apply(simp add: Graph10 BtoW_def)
     apply(rule disjI2, clarify, erule less_SucE, force)
     apply(case_tac "M x!snd(E x! ind x)=Black")
      apply(force)
     apply(force)
    apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
    --{* 3 subgoals left *}
    apply force
    --{* 2 subgoals left *}
    apply clarify
    apply(conjI_tac)
    apply(disjE_tac)
     apply (simp_all)
    apply clarify
    apply(erule less_SucE)
     apply force
    apply (simp add:BtoW_def)
    --{* 1 subgoal left *}
    apply clarify
    apply simp
    apply(disjE_tac)
    apply (simp_all)
    apply(rule disjI1 , rule Graph1)
     apply simp_all
    done

    subsubsection {* Counting Black Nodes *}

    constdefs
      Mul_CountInv :: "mul_gar_coll_state => nat => bool"
     "Mul_CountInv ≡ « λind. {i. i<ind ∧ ´Ma!i=Black}⊆´bc »"

      Mul_Count :: "nat =>  mul_gar_coll_state ann_com"
      "Mul_Count n ≡
      .{´Mul_Proper n ∧ Roots⊆Blacks ´M
        ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M
        ∧ length ´Ma=length ´M
        ∧ (´Safe ∨ ´obc⊂Blacks ´Ma ∨ ´l<´q ∧ (´q≤´Queue ∨ ´obc⊂Blacks ´M) )
        ∧ ´q<n+1 ∧ ´bc={}}.
      ´ind:=0;;
      .{´Mul_Proper n ∧ Roots⊆Blacks ´M
        ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M
        ∧ length ´Ma=length ´M
        ∧ (´Safe ∨ ´obc⊂Blacks ´Ma ∨ ´l<´q ∧ (´q≤´Queue ∨ ´obc⊂Blacks ´M) )
        ∧ ´q<n+1 ∧ ´bc={} ∧ ´ind=0}.
      WHILE ´ind<length ´M
         INV .{´Mul_Proper n ∧ Roots⊆Blacks ´M
              ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M
              ∧ length ´Ma=length ´M ∧ ´Mul_CountInv ´ind
              ∧ (´Safe ∨ ´obc⊂Blacks ´Ma ∨ ´l<´q ∧ (´q≤´Queue ∨ ´obc⊂Blacks ´M))
              ∧ ´q<n+1 ∧ ´ind≤length ´M}.
      DO .{´Mul_Proper n ∧ Roots⊆Blacks ´M
           ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M
           ∧ length ´Ma=length ´M ∧ ´Mul_CountInv ´ind
           ∧ (´Safe ∨ ´obc⊂Blacks ´Ma ∨ ´l<´q ∧ (´q≤´Queue ∨ ´obc⊂Blacks ´M))
           ∧ ´q<n+1 ∧ ´ind<length ´M}.
         IF ´M!´ind=Black
         THEN .{´Mul_Proper n ∧ Roots⊆Blacks ´M
                ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M
                ∧ length ´Ma=length ´M ∧ ´Mul_CountInv ´ind
                ∧ (´Safe ∨ ´obc⊂Blacks ´Ma ∨ ´l<´q ∧ (´q≤´Queue ∨ ´obc⊂Blacks ´M))
                ∧ ´q<n+1 ∧ ´ind<length ´M ∧ ´M!´ind=Black}.
              ´bc:=insert ´ind ´bc
         FI;;
      .{´Mul_Proper n ∧ Roots⊆Blacks ´M
        ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M
        ∧ length ´Ma=length ´M ∧ ´Mul_CountInv (´ind+1)
        ∧ (´Safe ∨ ´obc⊂Blacks ´Ma ∨ ´l<´q ∧ (´q≤´Queue ∨ ´obc⊂Blacks ´M))
        ∧ ´q<n+1 ∧ ´ind<length ´M}.
      ´ind:=´ind+1
      OD"

    lemma Mul_Count:
      "\<turnstile> Mul_Count n
      .{´Mul_Proper n ∧ Roots⊆Blacks ´M
        ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M
        ∧ length ´Ma=length ´M ∧ Blacks ´Ma⊆´bc
        ∧ (´Safe ∨ ´obc⊂Blacks ´Ma ∨ ´l<´q ∧ (´q≤´Queue ∨ ´obc⊂Blacks ´M))
        ∧ ´q<n+1}."
    apply (unfold Mul_Count_def)
    apply annhoare
    apply(simp_all add:Mul_CountInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def)
    --{* 7 subgoals left *}
    apply force
    apply force
    apply force
    --{* 4 subgoals left *}
    apply clarify
    apply(conjI_tac)
    apply(disjE_tac)
     apply simp_all
    apply(simp add:Blacks_def)
    apply clarify
    apply(erule less_SucE)
     back
     apply force
    apply force
    --{* 3 subgoals left *}
    apply clarify
    apply(conjI_tac)
    apply(disjE_tac)
     apply simp_all
    apply clarify
    apply(erule less_SucE)
     back
     apply force
    apply simp
    apply(rotate_tac -1)
    apply (force simp add:Blacks_def)
    --{* 2 subgoals left *}
    apply force
    --{* 1 subgoal left *}
    apply clarify
    apply(drule le_imp_less_or_eq)
    apply(disjE_tac)
    apply (simp_all add:Blacks_def)
    done

    subsubsection {* Appending garbage nodes to the free list *}

    consts  Append_to_free :: "nat × edges => edges"

    axioms
      Append_to_free0: "length (Append_to_free (i, e)) = length e"
      Append_to_free1: "Proper_Edges (m, e)
                        ==> Proper_Edges (m, Append_to_free(i, e))"
      Append_to_free2: "i ∉ Reach e
               ==> n ∈ Reach (Append_to_free(i, e)) = ( n = i ∨ n ∈ Reach e)"

    constdefs
      Mul_AppendInv :: "mul_gar_coll_state => nat => bool"
      "Mul_AppendInv ≡ « λind. (∀i. ind≤i --> i<length ´M --> i∈Reach ´E --> ´M!i=Black)»"

      Mul_Append :: "nat =>  mul_gar_coll_state ann_com"
      "Mul_Append n ≡
      .{´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´Safe}.
      ´ind:=0;;
      .{´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´Safe ∧ ´ind=0}.
      WHILE ´ind<length ´M
        INV .{´Mul_Proper n ∧ ´Mul_AppendInv ´ind ∧ ´ind≤length ´M}.
      DO .{´Mul_Proper n ∧ ´Mul_AppendInv ´ind ∧ ´ind<length ´M}.
          IF ´M!´ind=Black THEN
         .{´Mul_Proper n ∧ ´Mul_AppendInv ´ind ∧ ´ind<length ´M ∧ ´M!´ind=Black}.
          ´M:=´M[´ind:=White]
          ELSE
         .{´Mul_Proper n ∧ ´Mul_AppendInv ´ind ∧ ´ind<length ´M ∧ ´ind∉Reach ´E}.
          ´E:=Append_to_free(´ind,´E)
          FI;;
      .{´Mul_Proper n ∧ ´Mul_AppendInv (´ind+1) ∧ ´ind<length ´M}.
       ´ind:=´ind+1
      OD"

    lemma Mul_Append:
      "\<turnstile> Mul_Append n
         .{´Mul_Proper n}."
    apply(unfold Mul_Append_def)
    apply annhoare
    apply(simp_all add: mul_collector_defs Mul_AppendInv_def
          Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
    apply(force simp add:Blacks_def)
    apply(force simp add:Blacks_def)
    apply(force simp add:Blacks_def)
    apply(force simp add:Graph_defs)
    apply force
    apply(force simp add:Append_to_free1 Append_to_free2)
    apply force
    apply force
    done

    subsubsection {* Collector *}

    constdefs
      Mul_Collector :: "nat =>  mul_gar_coll_state ann_com"
      "Mul_Collector n ≡
    .{´Mul_Proper n}.
    WHILE True INV .{´Mul_Proper n}.
    DO
    Mul_Blacken_Roots n ;;
    .{´Mul_Proper n ∧ Roots⊆Blacks ´M}.
     ´obc:={};;
    .{´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´obc={}}.
     ´bc:=Roots;;
    .{´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´obc={} ∧ ´bc=Roots}.
     ´l:=0;;
    .{´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´obc={} ∧ ´bc=Roots ∧ ´l=0}.
     WHILE ´l<n+1
       INV .{´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧
             (´Safe ∨ (´l≤´Queue ∨ ´bc⊂Blacks ´M) ∧ ´l<n+1)}.
     DO .{´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´bc⊆Blacks ´M
          ∧ (´Safe ∨ ´l≤´Queue ∨ ´bc⊂Blacks ´M)}.
        ´obc:=´bc;;
        Mul_Propagate_Black n;;
        .{´Mul_Proper n ∧ Roots⊆Blacks ´M
          ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M
          ∧ (´Safe ∨ ´obc⊂Blacks ´M ∨ ´l<´Queue
          ∧ (´l≤´Queue ∨ ´obc⊂Blacks ´M))}.
        ´bc:={};;
        .{´Mul_Proper n ∧ Roots⊆Blacks ´M
          ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M
          ∧ (´Safe ∨ ´obc⊂Blacks ´M ∨ ´l<´Queue
          ∧ (´l≤´Queue ∨ ´obc⊂Blacks ´M)) ∧ ´bc={}}.
           ⟨ ´Ma:=´M,, ´q:=´Queue ⟩;;
        Mul_Count n;;
        .{´Mul_Proper n ∧ Roots⊆Blacks ´M
          ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M
          ∧ length ´Ma=length ´M ∧ Blacks ´Ma⊆´bc
          ∧ (´Safe ∨ ´obc⊂Blacks ´Ma ∨ ´l<´q ∧ (´q≤´Queue ∨ ´obc⊂Blacks ´M))
          ∧ ´q<n+1}.
        IF ´obc=´bc THEN
        .{´Mul_Proper n ∧ Roots⊆Blacks ´M
          ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M
          ∧ length ´Ma=length ´M ∧ Blacks ´Ma⊆´bc
          ∧ (´Safe ∨ ´obc⊂Blacks ´Ma ∨ ´l<´q ∧ (´q≤´Queue ∨ ´obc⊂Blacks ´M))
          ∧ ´q<n+1 ∧ ´obc=´bc}.
        ´l:=´l+1
        ELSE .{´Mul_Proper n ∧ Roots⊆Blacks ´M
              ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M
              ∧ length ´Ma=length ´M ∧ Blacks ´Ma⊆´bc
              ∧ (´Safe ∨ ´obc⊂Blacks ´Ma ∨ ´l<´q ∧ (´q≤´Queue ∨ ´obc⊂Blacks ´M))
              ∧ ´q<n+1 ∧ ´obc≠´bc}.
            ´l:=0 FI
     OD;;
     Mul_Append n
    OD"

    lemmas mul_modules = Mul_Redirect_Edge_def Mul_Color_Target_def
     Mul_Blacken_Roots_def Mul_Propagate_Black_def
     Mul_Count_def Mul_Append_def

    lemma Mul_Collector:
      "\<turnstile> Mul_Collector n
      .{False}."
    apply(unfold Mul_Collector_def)
    apply annhoare
    apply(simp_all only:pre.simps Mul_Blacken_Roots
           Mul_Propagate_Black Mul_Count Mul_Append)
    apply(simp_all add:mul_modules)
    apply(simp_all add:mul_collector_defs Queue_def)
    apply force
    apply force
    apply force
    apply (force simp add: less_Suc_eq_le)
    apply force
    apply (force dest:subset_antisym)
    apply force
    apply force
    apply force
    done

    subsection {* Interference Freedom *}

    lemma le_length_filter_update[rule_format]:
     "∀i. (¬P (list!i) ∨ P j) ∧ i<length list
     --> length(filter P list) ≤ length(filter P (list[i:=j]))"
    apply(induct_tac "list")
     apply(simp)
    apply(clarify)
    apply(case_tac i)
     apply(simp)
    apply(simp)
    done

    lemma less_length_filter_update [rule_format]:
     "∀i. P j ∧ ¬(P (list!i)) ∧ i<length list
     --> length(filter P list) < length(filter P (list[i:=j]))"
    apply(induct_tac "list")
     apply(simp)
    apply(clarify)
    apply(case_tac i)
     apply(simp)
    apply(simp)
    done

    lemma Mul_interfree_Blacken_Roots_Redirect_Edge: "[|0≤j; j<n|] ==>
      interfree_aux (Some(Mul_Blacken_Roots n),{},Some(Mul_Redirect_Edge j n))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply safe
    apply(simp_all add:Graph6 Graph9 Graph12 nth_list_update mul_mutator_defs mul_collector_defs)
    done

    lemma Mul_interfree_Redirect_Edge_Blacken_Roots: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Redirect_Edge j n ),{},Some (Mul_Blacken_Roots n))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply safe
    apply(simp_all add:mul_mutator_defs nth_list_update)
    done

    lemma Mul_interfree_Blacken_Roots_Color_Target: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Blacken_Roots n),{},Some (Mul_Color_Target j n ))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply safe
    apply(simp_all add:mul_mutator_defs mul_collector_defs nth_list_update Graph7 Graph8 Graph9 Graph12)
    done

    lemma Mul_interfree_Color_Target_Blacken_Roots: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Color_Target j n ),{},Some (Mul_Blacken_Roots n ))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply safe
    apply(simp_all add:mul_mutator_defs nth_list_update)
    done

    lemma Mul_interfree_Propagate_Black_Redirect_Edge: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Propagate_Black n),{},Some (Mul_Redirect_Edge j n ))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_PBInv_def nth_list_update Graph6)
    --{* 7 subgoals left *}
    apply clarify
    apply(disjE_tac)
      apply(simp_all add:Graph6)
     apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
    apply(rule conjI)
     apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    --{* 6 subgoals left *}
    apply clarify
    apply(disjE_tac)
      apply(simp_all add:Graph6)
     apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
    apply(rule conjI)
     apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    --{* 5 subgoals left *}
    apply clarify
    apply(disjE_tac)
      apply(simp_all add:Graph6)
     apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
    apply(rule conjI)
     apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(erule conjE)
    apply(case_tac "M x!(T (Muts x!j))=Black")
     apply(rule conjI)
      apply(rule impI,(rule disjI2)+,rule conjI)
       apply clarify
       apply(case_tac "R (Muts x! j)=i")
        apply (force simp add: nth_list_update BtoW_def)
       apply (force simp add: nth_list_update)
      apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
     apply(rule impI,(rule disjI2)+, erule le_trans)
     apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(rule conjI)
     apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
     apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
    apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
    apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
    --{* 4 subgoals left *}
    apply clarify
    apply(disjE_tac)
      apply(simp_all add:Graph6)
     apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
    apply(rule conjI)
     apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(erule conjE)
    apply(case_tac "M x!(T (Muts x!j))=Black")
     apply(rule conjI)
      apply(rule impI,(rule disjI2)+,rule conjI)
       apply clarify
       apply(case_tac "R (Muts x! j)=i")
        apply (force simp add: nth_list_update BtoW_def)
       apply (force simp add: nth_list_update)
      apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
     apply(rule impI,(rule disjI2)+, erule le_trans)
     apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(rule conjI)
     apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
     apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
    apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
    apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
    --{* 3 subgoals left *}
    apply clarify
    apply(disjE_tac)
      apply(simp_all add:Graph6)
      apply (rule impI)
       apply(rule conjI)
        apply(rule disjI1,rule subset_trans,erule Graph3,simp,simp)
       apply(case_tac "R (Muts x ! j)= ind x")
        apply(simp add:nth_list_update)
       apply(simp add:nth_list_update)
      apply(case_tac "R (Muts x ! j)= ind x")
       apply(simp add:nth_list_update)
      apply(simp add:nth_list_update)
     apply(case_tac "M x!(T (Muts x!j))=Black")
      apply(rule conjI)
       apply(rule impI)
       apply(rule conjI)
        apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
        apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
       apply(case_tac "R (Muts x ! j)= ind x")
        apply(simp add:nth_list_update)
       apply(simp add:nth_list_update)
      apply(rule impI)
      apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
     apply(rule conjI)
      apply(rule impI)
       apply(rule conjI)
        apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
        apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
       apply(case_tac "R (Muts x ! j)= ind x")
        apply(simp add:nth_list_update)
       apply(simp add:nth_list_update)
      apply(rule impI)
      apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
     apply(erule conjE)
     apply(rule conjI)
      apply(case_tac "M x!(T (Muts x!j))=Black")
       apply(rule impI,rule conjI,(rule disjI2)+,rule conjI)
        apply clarify
        apply(case_tac "R (Muts x! j)=i")
         apply (force simp add: nth_list_update BtoW_def)
        apply (force simp add: nth_list_update)
       apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
      apply(case_tac "R (Muts x ! j)= ind x")
       apply(simp add:nth_list_update)
      apply(simp add:nth_list_update)
     apply(rule impI,rule conjI)
      apply(rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
      apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
     apply(case_tac "R (Muts x! j)=ind x")
      apply (force simp add: nth_list_update)
     apply (force simp add: nth_list_update)
    apply(rule impI, (rule disjI2)+, erule le_trans)
    apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    --{* 2 subgoals left *}
    apply clarify
    apply(rule conjI)
     apply(disjE_tac)
      apply(simp_all add:Mul_Auxk_def Graph6)
      apply (rule impI)
       apply(rule conjI)
        apply(rule disjI1,rule subset_trans,erule Graph3,simp,simp)
       apply(case_tac "R (Muts x ! j)= ind x")
        apply(simp add:nth_list_update)
       apply(simp add:nth_list_update)
      apply(case_tac "R (Muts x ! j)= ind x")
       apply(simp add:nth_list_update)
      apply(simp add:nth_list_update)
     apply(case_tac "M x!(T (Muts x!j))=Black")
      apply(rule impI)
      apply(rule conjI)
       apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
       apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
      apply(case_tac "R (Muts x ! j)= ind x")
       apply(simp add:nth_list_update)
      apply(simp add:nth_list_update)
     apply(rule impI)
     apply(rule conjI)
      apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
     apply(case_tac "R (Muts x ! j)= ind x")
      apply(simp add:nth_list_update)
     apply(simp add:nth_list_update)
    apply(rule impI)
    apply(rule conjI)
     apply(erule conjE)+
     apply(case_tac "M x!(T (Muts x!j))=Black")
      apply((rule disjI2)+,rule conjI)
       apply clarify
       apply(case_tac "R (Muts x! j)=i")
        apply (force simp add: nth_list_update BtoW_def)
       apply (force simp add: nth_list_update)
      apply(rule conjI)
       apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
      apply(rule impI)
      apply(case_tac "R (Muts x ! j)= ind x")
       apply(simp add:nth_list_update BtoW_def)
      apply (simp  add:nth_list_update)
      apply(rule impI)
      apply simp
      apply(disjE_tac)
       apply(rule disjI1, erule less_le_trans)
       apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
      apply force
     apply(rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
     apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
     apply(case_tac "R (Muts x ! j)= ind x")
      apply(simp add:nth_list_update)
     apply(simp add:nth_list_update)
    apply(disjE_tac)
    apply simp_all
    apply(conjI_tac)
     apply(rule impI)
     apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
     apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(erule conjE)+
    apply(rule impI,(rule disjI2)+,rule conjI)
     apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(rule impI)+
    apply simp
    apply(disjE_tac)
     apply(rule disjI1, erule less_le_trans)
     apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply force
    --{* 1 subgoal left *}
    apply clarify
    apply(disjE_tac)
      apply(simp_all add:Graph6)
     apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
    apply(rule conjI)
     apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(erule conjE)
    apply(case_tac "M x!(T (Muts x!j))=Black")
     apply(rule conjI)
      apply(rule impI,(rule disjI2)+,rule conjI)
       apply clarify
       apply(case_tac "R (Muts x! j)=i")
        apply (force simp add: nth_list_update BtoW_def)
       apply (force simp add: nth_list_update)
      apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
     apply(rule impI,(rule disjI2)+, erule le_trans)
     apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(rule conjI)
     apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
     apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
    apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
    apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
    done

    lemma Mul_interfree_Redirect_Edge_Propagate_Black: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Redirect_Edge j n ),{},Some (Mul_Propagate_Black n))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply safe
    apply(simp_all add:mul_mutator_defs nth_list_update)
    done

    lemma Mul_interfree_Propagate_Black_Color_Target: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Propagate_Black n),{},Some (Mul_Color_Target j n ))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply(simp_all add: mul_collector_defs mul_mutator_defs)
    --{* 7 subgoals left *}
    apply clarify
    apply (simp add:Graph7 Graph8 Graph12)
    apply(disjE_tac)
      apply(simp add:Graph7 Graph8 Graph12)
     apply(case_tac "M x!(T (Muts x!j))=Black")
      apply(rule disjI2,rule disjI1, erule le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
     apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp)
    apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
    --{* 6 subgoals left *}
    apply clarify
    apply (simp add:Graph7 Graph8 Graph12)
    apply(disjE_tac)
      apply(simp add:Graph7 Graph8 Graph12)
     apply(case_tac "M x!(T (Muts x!j))=Black")
      apply(rule disjI2,rule disjI1, erule le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
     apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp)
    apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
    --{* 5 subgoals left *}
    apply clarify
    apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
    apply(disjE_tac)
       apply(simp add:Graph7 Graph8 Graph12)
      apply(rule disjI2,rule disjI1, erule psubset_subset_trans,simp add:Graph9)
     apply(case_tac "M x!(T (Muts x!j))=Black")
      apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
     apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
    apply(erule conjE)
    apply(case_tac "M x!(T (Muts x!j))=Black")
     apply((rule disjI2)+)
     apply (rule conjI)
      apply(simp add:Graph10)
     apply(erule le_trans)
     apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
    apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
    --{* 4 subgoals left *}
    apply clarify
    apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
    apply(disjE_tac)
       apply(simp add:Graph7 Graph8 Graph12)
      apply(rule disjI2,rule disjI1, erule psubset_subset_trans,simp add:Graph9)
     apply(case_tac "M x!(T (Muts x!j))=Black")
      apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
     apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
    apply(erule conjE)
    apply(case_tac "M x!(T (Muts x!j))=Black")
     apply((rule disjI2)+)
     apply (rule conjI)
      apply(simp add:Graph10)
     apply(erule le_trans)
     apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
    apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
    --{* 3 subgoals left *}
    apply clarify
    apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
    apply(case_tac "M x!(T (Muts x!j))=Black")
     apply(simp add:Graph10)
     apply(disjE_tac)
      apply simp_all
      apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
     apply(erule conjE)
     apply((rule disjI2)+,erule le_trans)
     apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
    apply(rule conjI)
     apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11)
    apply (force simp add:nth_list_update)
    --{* 2 subgoals left *}
    apply clarify
    apply(simp add:Mul_Auxk_def Graph7 Graph8 Graph12)
    apply(case_tac "M x!(T (Muts x!j))=Black")
     apply(simp add:Graph10)
     apply(disjE_tac)
      apply simp_all
      apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
     apply(erule conjE)+
     apply((rule disjI2)+,rule conjI, erule le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
     apply((rule impI)+)
     apply simp
     apply(erule disjE)
      apply(rule disjI1, erule less_le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
     apply force
    apply(rule conjI)
     apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11)
    apply (force simp add:nth_list_update)
    --{* 1 subgoal left *}
    apply clarify
    apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
    apply(case_tac "M x!(T (Muts x!j))=Black")
     apply(simp add:Graph10)
     apply(disjE_tac)
      apply simp_all
      apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
     apply(erule conjE)
     apply((rule disjI2)+,erule le_trans)
     apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
    apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11)
    done

    lemma Mul_interfree_Color_Target_Propagate_Black: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Color_Target j n),{},Some(Mul_Propagate_Black n ))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply safe
    apply(simp_all add:mul_mutator_defs nth_list_update)
    done

    lemma Mul_interfree_Count_Redirect_Edge: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Count n ),{},Some(Mul_Redirect_Edge j n))"
    apply (unfold mul_modules)
    apply interfree_aux
    --{* 9 subgoals left *}
    apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def Graph6)
    apply clarify
    apply disjE_tac
       apply(simp add:Graph6)
      apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
     apply(simp add:Graph6)
    apply clarify
    apply disjE_tac
     apply(simp add:Graph6)
     apply(rule conjI)
      apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
     apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(simp add:Graph6)
    --{* 8 subgoals left *}
    apply(simp add:mul_mutator_defs nth_list_update)
    --{* 7 subgoals left *}
    apply(simp add:mul_mutator_defs mul_collector_defs)
    apply clarify
    apply disjE_tac
       apply(simp add:Graph6)
      apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
     apply(simp add:Graph6)
    apply clarify
    apply disjE_tac
     apply(simp add:Graph6)
     apply(rule conjI)
      apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
     apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(simp add:Graph6)
    --{* 6 subgoals left *}
    apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
    apply clarify
    apply disjE_tac
       apply(simp add:Graph6 Queue_def)
      apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
     apply(simp add:Graph6)
    apply clarify
    apply disjE_tac
     apply(simp add:Graph6)
     apply(rule conjI)
      apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
     apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(simp add:Graph6)
    --{* 5 subgoals left *}
    apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
    apply clarify
    apply disjE_tac
       apply(simp add:Graph6)
      apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
     apply(simp add:Graph6)
    apply clarify
    apply disjE_tac
     apply(simp add:Graph6)
     apply(rule conjI)
      apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
     apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(simp add:Graph6)
    --{* 4 subgoals left *}
    apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
    apply clarify
    apply disjE_tac
       apply(simp add:Graph6)
      apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
     apply(simp add:Graph6)
    apply clarify
    apply disjE_tac
     apply(simp add:Graph6)
     apply(rule conjI)
      apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
     apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(simp add:Graph6)
    --{* 3 subgoals left *}
    apply(simp add:mul_mutator_defs nth_list_update)
    --{* 2 subgoals left *}
    apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
    apply clarify
    apply disjE_tac
       apply(simp add:Graph6)
      apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
     apply(simp add:Graph6)
    apply clarify
    apply disjE_tac
     apply(simp add:Graph6)
     apply(rule conjI)
      apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
     apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(simp add:Graph6)
    --{* 1 subgoal left *}
    apply(simp add:mul_mutator_defs nth_list_update)
    done

    lemma Mul_interfree_Redirect_Edge_Count: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Count n ))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply safe
    apply(simp_all add:mul_mutator_defs nth_list_update)
    done

    lemma Mul_interfree_Count_Color_Target: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Count n ),{},Some(Mul_Color_Target j n))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply(simp_all add:mul_collector_defs mul_mutator_defs Mul_CountInv_def)
    --{* 6 subgoals left *}
    apply clarify
    apply disjE_tac
      apply (simp add: Graph7 Graph8 Graph12)
     apply (simp add: Graph7 Graph8 Graph12)
    apply clarify
    apply disjE_tac
     apply (simp add: Graph7 Graph8 Graph12)
     apply(case_tac "M x!(T (Muts x!j))=Black")
      apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
     apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
    apply (simp add: Graph7 Graph8 Graph12)
    apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
    --{* 5 subgoals left *}
    apply clarify
    apply disjE_tac
      apply (simp add: Graph7 Graph8 Graph12)
     apply (simp add: Graph7 Graph8 Graph12)
    apply clarify
    apply disjE_tac
     apply (simp add: Graph7 Graph8 Graph12)
     apply(case_tac "M x!(T (Muts x!j))=Black")
      apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
     apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
    apply (simp add: Graph7 Graph8 Graph12)
    apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
    --{* 4 subgoals left *}
    apply clarify
    apply disjE_tac
      apply (simp add: Graph7 Graph8 Graph12)
     apply (simp add: Graph7 Graph8 Graph12)
    apply clarify
    apply disjE_tac
     apply (simp add: Graph7 Graph8 Graph12)
     apply(case_tac "M x!(T (Muts x!j))=Black")
      apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
     apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
    apply (simp add: Graph7 Graph8 Graph12)
    apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
    --{* 3 subgoals left *}
    apply clarify
    apply disjE_tac
      apply (simp add: Graph7 Graph8 Graph12)
     apply (simp add: Graph7 Graph8 Graph12)
    apply clarify
    apply disjE_tac
     apply (simp add: Graph7 Graph8 Graph12)
     apply(case_tac "M x!(T (Muts x!j))=Black")
      apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
     apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
    apply (simp add: Graph7 Graph8 Graph12)
    apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
    --{* 2 subgoals left *}
    apply clarify
    apply disjE_tac
      apply (simp add: Graph7 Graph8 Graph12 nth_list_update)
     apply (simp add: Graph7 Graph8 Graph12 nth_list_update)
    apply clarify
    apply disjE_tac
     apply (simp add: Graph7 Graph8 Graph12)
     apply(rule conjI)
      apply(case_tac "M x!(T (Muts x!j))=Black")
       apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
       apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
      apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
     apply (simp add: nth_list_update)
    apply (simp add: Graph7 Graph8 Graph12)
    apply(rule conjI)
     apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
    apply (simp add: nth_list_update)
    --{* 1 subgoal left *}
    apply clarify
    apply disjE_tac
      apply (simp add: Graph7 Graph8 Graph12)
     apply (simp add: Graph7 Graph8 Graph12)
    apply clarify
    apply disjE_tac
     apply (simp add: Graph7 Graph8 Graph12)
     apply(case_tac "M x!(T (Muts x!j))=Black")
      apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
      apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
     apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
    apply (simp add: Graph7 Graph8 Graph12)
    apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
    done

    lemma Mul_interfree_Color_Target_Count: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Count n ))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply safe
    apply(simp_all add:mul_mutator_defs nth_list_update)
    done

    lemma Mul_interfree_Append_Redirect_Edge: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Append n),{}, Some(Mul_Redirect_Edge j n))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply(tactic {* ALLGOALS Clarify_tac *})
    apply(simp_all add:Graph6 Append_to_free0 Append_to_free1 mul_collector_defs mul_mutator_defs Mul_AppendInv_def)
    apply(erule_tac x=j in allE, force dest:Graph3)+
    done

    lemma Mul_interfree_Redirect_Edge_Append: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Append n))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply(tactic {* ALLGOALS Clarify_tac *})
    apply(simp_all add:mul_collector_defs Append_to_free0 Mul_AppendInv_def  mul_mutator_defs nth_list_update)
    done

    lemma Mul_interfree_Append_Color_Target: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Append n),{}, Some(Mul_Color_Target j n))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply(tactic {* ALLGOALS Clarify_tac *})
    apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_AppendInv_def Graph7 Graph8 Append_to_free0 Append_to_free1
                  Graph12 nth_list_update)
    done

    lemma Mul_interfree_Color_Target_Append: "[|0≤j; j<n|]==>
      interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Append n))"
    apply (unfold mul_modules)
    apply interfree_aux
    apply(tactic {* ALLGOALS Clarify_tac *})
    apply(simp_all add: mul_mutator_defs nth_list_update)
    apply(simp add:Mul_AppendInv_def Append_to_free0)
    done

    subsubsection {* Interference freedom Collector-Mutator *}

    lemmas mul_collector_mutator_interfree =
     Mul_interfree_Blacken_Roots_Redirect_Edge Mul_interfree_Blacken_Roots_Color_Target
     Mul_interfree_Propagate_Black_Redirect_Edge Mul_interfree_Propagate_Black_Color_Target
     Mul_interfree_Count_Redirect_Edge Mul_interfree_Count_Color_Target
     Mul_interfree_Append_Redirect_Edge Mul_interfree_Append_Color_Target
     Mul_interfree_Redirect_Edge_Blacken_Roots Mul_interfree_Color_Target_Blacken_Roots
     Mul_interfree_Redirect_Edge_Propagate_Black Mul_interfree_Color_Target_Propagate_Black
     Mul_interfree_Redirect_Edge_Count Mul_interfree_Color_Target_Count
     Mul_interfree_Redirect_Edge_Append Mul_interfree_Color_Target_Append

    lemma Mul_interfree_Collector_Mutator: "j<n  ==>
      interfree_aux (Some (Mul_Collector n), {}, Some (Mul_Mutator j n))"
    apply(unfold Mul_Collector_def Mul_Mutator_def)
    apply interfree_aux
    apply(simp_all add:mul_collector_mutator_interfree)
    apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
    apply(tactic  {* TRYALL (interfree_aux_tac) *})
    --{* 42 subgoals left *}
    apply (clarify,simp add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)+
    --{* 24 subgoals left *}
    apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
    --{* 14 subgoals left *}
    apply(tactic {* TRYALL Clarify_tac *})
    apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
    apply(tactic {* TRYALL (rtac conjI) *})
    apply(tactic {* TRYALL (rtac impI) *})
    apply(tactic {* TRYALL (etac disjE) *})
    apply(tactic {* TRYALL (etac conjE) *})
    apply(tactic {* TRYALL (etac disjE) *})
    apply(tactic {* TRYALL (etac disjE) *})
    --{* 72 subgoals left *}
    apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
    --{* 35 subgoals left *}
    apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac (thm "Graph3"),Force_tac, assume_tac]) *})
    --{* 28 subgoals left *}
    apply(tactic {* TRYALL (etac conjE) *})
    apply(tactic {* TRYALL (etac disjE) *})
    --{* 34 subgoals left *}
    apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    apply(tactic {* ALLGOALS(case_tac "M x!(T (Muts x ! j))=Black") *})
    apply(simp_all add:Graph10)
    --{* 47 subgoals left *}
    apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac subset_psubset_trans,etac (thm "Graph11"),Force_tac]) *})
    --{* 41 subgoals left *}
    apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac le_trans, force_tac (claset(),simpset() addsimps [thm "Queue_def", less_Suc_eq_le, thm "le_length_filter_update"])]) *})
    --{* 35 subgoals left *}
    apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),Force_tac]) *})
    --{* 31 subgoals left *}
    apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac subset_psubset_trans,etac (thm "Graph11"),Force_tac]) *})
    --{* 29 subgoals left *}
    apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac subset_psubset_trans,etac subset_psubset_trans,etac (thm "Graph11"),Force_tac]) *})
    --{* 25 subgoals left *}
    apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac le_trans, force_tac (claset(),simpset() addsimps [thm "Queue_def", less_Suc_eq_le, thm "le_length_filter_update"])]) *})
    --{* 10 subgoals left *}
    apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+
    done

    subsubsection {* Interference freedom Mutator-Collector *}

    lemma Mul_interfree_Mutator_Collector: " j < n ==>
      interfree_aux (Some (Mul_Mutator j n), {}, Some (Mul_Collector n))"
    apply(unfold Mul_Collector_def Mul_Mutator_def)
    apply interfree_aux
    apply(simp_all add:mul_collector_mutator_interfree)
    apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
    apply(tactic  {* TRYALL (interfree_aux_tac) *})
    --{* 76 subgoals left *}
    apply (clarify,simp add: nth_list_update)+
    --{* 56 subgoals left *}
    apply(clarify,simp add:Mul_AppendInv_def Append_to_free0 nth_list_update)+
    done

    subsubsection {* The Multi-Mutator Garbage Collection Algorithm *}

    text {* The total number of verification conditions is 328 *}

    lemma Mul_Gar_Coll:
     "\<parallel>- .{´Mul_Proper n ∧ ´Mul_mut_init n ∧ (∀i<n. Z (´Muts!i))}.
     COBEGIN
      Mul_Collector n
     .{False}.
     \<parallel>
     SCHEME  [0≤ j< n]
      Mul_Mutator j n
     .{False}.
     COEND
     .{False}."
    apply oghoare
    --{* Strengthening the precondition *}
    apply(rule Int_greatest)
     apply (case_tac n)
      apply(force simp add: Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
     apply(simp add: Mul_Mutator_def mul_collector_defs mul_mutator_defs nth_append)
     apply force
    apply clarify
    apply(case_tac xa)
     apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
    apply(simp add: Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append nth_map_upt)
    --{* Collector *}
    apply(rule Mul_Collector)
    --{* Mutator *}
    apply(erule Mul_Mutator)
    --{* Interference freedom *}
    apply(simp add:Mul_interfree_Collector_Mutator)
    apply(simp add:Mul_interfree_Mutator_Collector)
    apply(simp add:Mul_interfree_Mutator_Mutator)
    --{* Weakening of the postcondition *}
    apply(case_tac n)
     apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
    apply(simp add:Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append)
    done

    end

### The Mutators

lemmas mul_mutator_defs:

      Mul_mut_init ==
      %s n. n = length (Muts s) ∧
            (∀i<n. R (Muts s ! i) < length (E s) ∧ T (Muts s ! i) < length (M s))

      Mul_Redirect_Edge j n == .{´Mul_mut_init n ∧ Z (´Muts ! j)}.
      ⟨IF T (´Muts ! j)
          ∈ Reach
             ´E THEN ´E := ´E
                     [R (´Muts ! j) := (fst (´E ! R (´Muts ! j)), T (´Muts ! j))] FI,,
      ´Muts := ´Muts[j := (´Muts ! j)(| Z := False |)]⟩

      Mul_Color_Target j n == .{´Mul_mut_init n ∧ ¬ Z (´Muts ! j)}.
      ⟨´M := ´M[T (´Muts ! j) := Black],,
      ´Muts := ´Muts[j := (´Muts ! j)(| Z := True |)]⟩

lemmas mul_mutator_defs:

      Mul_mut_init ==
      %s n. n = length (Muts s) ∧
            (∀i<n. R (Muts s ! i) < length (E s) ∧ T (Muts s ! i) < length (M s))

      Mul_Redirect_Edge j n == .{´Mul_mut_init n ∧ Z (´Muts ! j)}.
      ⟨IF T (´Muts ! j)
          ∈ Reach
             ´E THEN ´E := ´E
                     [R (´Muts ! j) := (fst (´E ! R (´Muts ! j)), T (´Muts ! j))] FI,,
      ´Muts := ´Muts[j := (´Muts ! j)(| Z := False |)]⟩

      Mul_Color_Target j n == .{´Mul_mut_init n ∧ ¬ Z (´Muts ! j)}.
      ⟨´M := ´M[T (´Muts ! j) := Black],,
      ´Muts := ´Muts[j := (´Muts ! j)(| Z := True |)]⟩

#### Correctness of the proof outline of one mutator

lemma Mul_Redirect_Edge:

      0 ≤ j ∧ j < n
      ==> \<turnstile> Mul_Redirect_Edge j n
             pre (Mul_Color_Target j n)

lemma Mul_Color_Target:

      0 ≤ j ∧ j < n
      ==> \<turnstile> Mul_Color_Target j n
             .{´Mul_mut_init n ∧ Z (´Muts ! j)}.

lemma Mul_Mutator:

      0 ≤ j ∧ j < n ==> \<turnstile> Mul_Mutator j n
                           .{False}.

#### Interference freedom between mutators

lemma Mul_interfree_Redirect_Edge_Redirect_Edge:

      [| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |]
      ==> interfree_aux
           (Some (Mul_Redirect_Edge i n), {}, Some (Mul_Redirect_Edge j n))

lemma Mul_interfree_Redirect_Edge_Color_Target:

      [| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |]
      ==> interfree_aux
           (Some (Mul_Redirect_Edge i n), {}, Some (Mul_Color_Target j n))

lemma Mul_interfree_Color_Target_Redirect_Edge:

      [| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |]
      ==> interfree_aux
           (Some (Mul_Color_Target i n), {}, Some (Mul_Redirect_Edge j n))

lemma Mul_interfree_Color_Target_Color_Target:

      [| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |]
      ==> interfree_aux (Some (Mul_Color_Target i n), {}, Some (Mul_Color_Target j n))

lemmas mul_mutator_interfree:

      [| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |]
      ==> interfree_aux
           (Some (Mul_Redirect_Edge i n), {}, Some (Mul_Redirect_Edge j n))

      [| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |]
      ==> interfree_aux
           (Some (Mul_Redirect_Edge i n), {}, Some (Mul_Color_Target j n))

      [| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |]
      ==> interfree_aux
           (Some (Mul_Color_Target i n), {}, Some (Mul_Redirect_Edge j n))

      [| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |]
      ==> interfree_aux (Some (Mul_Color_Target i n), {}, Some (Mul_Color_Target j n))

lemmas mul_mutator_interfree:

      [| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |]
      ==> interfree_aux
           (Some (Mul_Redirect_Edge i n), {}, Some (Mul_Redirect_Edge j n))

      [| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |]
      ==> interfree_aux
           (Some (Mul_Redirect_Edge i n), {}, Some (Mul_Color_Target j n))

      [| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |]
      ==> interfree_aux
           (Some (Mul_Color_Target i n), {}, Some (Mul_Redirect_Edge j n))

      [| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |]
      ==> interfree_aux (Some (Mul_Color_Target i n), {}, Some (Mul_Color_Target j n))

lemma Mul_interfree_Mutator_Mutator:

      [| i < n; j < n; i ≠ j |]
      ==> interfree_aux (Some (Mul_Mutator i n), {}, Some (Mul_Mutator j n))

#### Modular Parameterized Mutators

lemma Mul_Parameterized_Mutators:

      0 < n
      ==> \<parallel>- .{´Mul_mut_init n ∧ (∀i<n. Z (´Muts ! i))}.
             COBEGIN
             SCHEME [0 ≤ j < n] Mul_Mutator j n
              .{False}.
             COEND
             .{False}.

### The Collector

lemmas mul_collector_defs:

      Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)

      Mul_Proper ==
      %s n. Proper_Roots (M s) ∧
            Proper_Edges (M s, E s) ∧ Proper_M_init s ∧ n = length (Muts s)

      Safe == %s. Reach (E s) ⊆ Blacks (M s)

lemmas mul_collector_defs:

      Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)

      Mul_Proper ==
      %s n. Proper_Roots (M s) ∧
            Proper_Edges (M s, E s) ∧ Proper_M_init s ∧ n = length (Muts s)

      Safe == %s. Reach (E s) ⊆ Blacks (M s)

#### Blackening Roots

lemma Mul_Blacken_Roots:

      \<turnstile> Mul_Blacken_Roots n
         .{´Mul_Proper n ∧ Roots ⊆ Blacks ´M}.

#### Propagating Black

lemma Mul_Propagate_Black:

      \<turnstile> Mul_Propagate_Black n
         .{´Mul_Proper n ∧
           Roots ⊆ Blacks ´M ∧
           ´obc ⊆ Blacks ´M ∧
           ´bc ⊆ Blacks ´M ∧
           (´Safe ∨
            ´obc ⊂ Blacks ´M ∨ ´l < ´Queue ∧ (´l ≤ ´Queue ∨ ´obc ⊂ Blacks ´M))}.

#### Counting Black Nodes

lemma Mul_Count:

      \<turnstile> Mul_Count n
         .{´Mul_Proper n ∧
           Roots ⊆ Blacks ´M ∧
           ´obc ⊆ Blacks ´Ma ∧
           Blacks ´Ma ⊆ Blacks ´M ∧
           ´bc ⊆ Blacks ´M ∧
           length ´Ma = length ´M ∧
           Blacks ´Ma ⊆ ´bc ∧
           (´Safe ∨ ´obc ⊂ Blacks ´Ma ∨ ´l < ´q ∧ (´q ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)) ∧
           ´q < n + 1}.

#### Appending garbage nodes to the free list

lemma Mul_Append:

      \<turnstile> Mul_Append n
         .{´Mul_Proper n}.

#### Collector

lemmas mul_modules:

      Mul_Redirect_Edge j n == .{´Mul_mut_init n ∧ Z (´Muts ! j)}.
      ⟨IF T (´Muts ! j)
          ∈ Reach
             ´E THEN ´E := ´E
                     [R (´Muts ! j) := (fst (´E ! R (´Muts ! j)), T (´Muts ! j))] FI,,
      ´Muts := ´Muts[j := (´Muts ! j)(| Z := False |)]⟩

      Mul_Color_Target j n == .{´Mul_mut_init n ∧ ¬ Z (´Muts ! j)}.
      ⟨´M := ´M[T (´Muts ! j) := Black],,
      ´Muts := ´Muts[j := (´Muts ! j)(| Z := True |)]⟩

      Mul_Blacken_Roots n == .{´Mul_Proper n}. ´ind := 0;;
      .{´Mul_Proper n ∧ ´ind = 0}.
      WHILE ´ind < length ´M
      INV .{´Mul_Proper n ∧
            (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧ ´ind ≤ length ´M}.
      DO .{´Mul_Proper n ∧
           (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧ ´ind < length ´M}.
      IF ´ind ∈ Roots
      THEN .{´Mul_Proper n ∧
             (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧
             ´ind < length ´M ∧ ´ind ∈ Roots}. ´M :=
           ´M[´ind := Black]
      FI;;
      .{´Mul_Proper n ∧
        (∀i<´ind + 1. i ∈ Roots --> ´M ! i = Black) ∧ ´ind < length ´M}. ´ind :=
      ´ind + 1
      OD

      Mul_Propagate_Black n ==
      .{´Mul_Proper n ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´M ∧
        ´bc ⊆ Blacks ´M ∧ (´Safe ∨ ´l ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)}. ´ind :=
      0;;
      .{´Mul_Proper n ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´M ∧
        Blacks ´M ⊆ Blacks ´M ∧
        ´bc ⊆ Blacks ´M ∧ (´Safe ∨ ´l ≤ ´Queue ∨ ´obc ⊂ Blacks ´M) ∧ ´ind = 0}.
      WHILE ´ind < length ´E
      INV .{´Mul_Proper n ∧
            Roots ⊆ Blacks ´M ∧
            ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´Mul_PBInv ∧ ´ind ≤ length ´E}.
      DO .{´Mul_Proper n ∧
           Roots ⊆ Blacks ´M ∧
           ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´Mul_PBInv ∧ ´ind < length ´E}.
      IF ´M ! fst (´E ! ´ind) = Black
      THEN .{´Mul_Proper n ∧
             Roots ⊆ Blacks ´M ∧
             ´obc ⊆ Blacks ´M ∧
             ´bc ⊆ Blacks ´M ∧
             ´Mul_PBInv ∧ ´M ! fst (´E ! ´ind) = Black ∧ ´ind < length ´E}. ´k :=
           snd (´E ! ´ind);;
      .{´Mul_Proper n ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´M ∧
        ´bc ⊆ Blacks ´M ∧
        (´Safe ∨
         ´obc ⊂ Blacks ´M ∨
         ´l < ´Queue ∨ (∀i<´ind. ¬ BtoW (´E ! i, ´M)) ∧ ´l ≤ ´Queue ∧ ´Mul_Auxk) ∧
        ´k < length ´M ∧ ´M ! fst (´E ! ´ind) = Black ∧ ´ind < length ´E}.
      ⟨´M := ´M[´k := Black],, ´ind := ´ind + 1⟩
      ELSE .{´Mul_Proper n ∧
             Roots ⊆ Blacks ´M ∧
             ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´Mul_PBInv ∧ ´ind < length ´E}.
      ⟨IF ´M ! fst (´E ! ´ind) ≠ Black THEN ´ind := ´ind + 1 FI⟩ FI
      OD

      Mul_Count n ==
      .{´Mul_Proper n ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´Ma ∧
        Blacks ´Ma ⊆ Blacks ´M ∧
        ´bc ⊆ Blacks ´M ∧
        length ´Ma = length ´M ∧
        (´Safe ∨ ´obc ⊂ Blacks ´Ma ∨ ´l < ´q ∧ (´q ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)) ∧
        ´q < n + 1 ∧ ´bc = {}}. ´ind :=
      0;;
      .{´Mul_Proper n ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´Ma ∧
        Blacks ´Ma ⊆ Blacks ´M ∧
        ´bc ⊆ Blacks ´M ∧
        length ´Ma = length ´M ∧
        (´Safe ∨ ´obc ⊂ Blacks ´Ma ∨ ´l < ´q ∧ (´q ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)) ∧
        ´q < n + 1 ∧ ´bc = {} ∧ ´ind = 0}.
      WHILE ´ind < length ´M
      INV .{´Mul_Proper n ∧
            Roots ⊆ Blacks ´M ∧
            ´obc ⊆ Blacks ´Ma ∧
            Blacks ´Ma ⊆ Blacks ´M ∧
            ´bc ⊆ Blacks ´M ∧
            length ´Ma = length ´M ∧
            ´Mul_CountInv ´ind ∧
            (´Safe ∨ ´obc ⊂ Blacks ´Ma ∨ ´l < ´q ∧ (´q ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)) ∧
            ´q < n + 1 ∧ ´ind ≤ length ´M}.
      DO .{´Mul_Proper n ∧
           Roots ⊆ Blacks ´M ∧
           ´obc ⊆ Blacks ´Ma ∧
           Blacks ´Ma ⊆ Blacks ´M ∧
           ´bc ⊆ Blacks ´M ∧
           length ´Ma = length ´M ∧
           ´Mul_CountInv ´ind ∧
           (´Safe ∨ ´obc ⊂ Blacks ´Ma ∨ ´l < ´q ∧ (´q ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)) ∧
           ´q < n + 1 ∧ ´ind < length ´M}.
      IF ´M ! ´ind = Black
      THEN .{´Mul_Proper n ∧
             Roots ⊆ Blacks ´M ∧
             ´obc ⊆ Blacks ´Ma ∧
             Blacks ´Ma ⊆ Blacks ´M ∧
             ´bc ⊆ Blacks ´M ∧
             length ´Ma = length ´M ∧
             ´Mul_CountInv ´ind ∧
             (´Safe ∨
              ´obc ⊂ Blacks ´Ma ∨ ´l < ´q ∧ (´q ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)) ∧
             ´q < n + 1 ∧ ´ind < length ´M ∧ ´M ! ´ind = Black}. ´bc :=
           insert ´ind ´bc
      FI;;
      .{´Mul_Proper n ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´Ma ∧
        Blacks ´Ma ⊆ Blacks ´M ∧
        ´bc ⊆ Blacks ´M ∧
        length ´Ma = length ´M ∧
        ´Mul_CountInv (´ind + 1) ∧
        (´Safe ∨ ´obc ⊂ Blacks ´Ma ∨ ´l < ´q ∧ (´q ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)) ∧
        ´q < n + 1 ∧ ´ind < length ´M}. ´ind :=
      ´ind + 1
      OD

      Mul_Append n == .{´Mul_Proper n ∧ Roots ⊆ Blacks ´M ∧ ´Safe}. ´ind := 0;;
      .{´Mul_Proper n ∧ Roots ⊆ Blacks ´M ∧ ´Safe ∧ ´ind = 0}.
      WHILE ´ind < length ´M
      INV .{´Mul_Proper n ∧ ´Mul_AppendInv ´ind ∧ ´ind ≤ length ´M}.
      DO .{´Mul_Proper n ∧ ´Mul_AppendInv ´ind ∧ ´ind < length ´M}.
      IF ´M ! ´ind = Black
      THEN .{´Mul_Proper n ∧
             ´Mul_AppendInv ´ind ∧ ´ind < length ´M ∧ ´M ! ´ind = Black}. ´M :=
           ´M[´ind := White]
      ELSE .{´Mul_Proper n ∧
             ´Mul_AppendInv ´ind ∧ ´ind < length ´M ∧ ´ind ∉ Reach ´E}. ´E :=
           Append_to_free (´ind, ´E)
      FI;;
      .{´Mul_Proper n ∧ ´Mul_AppendInv (´ind + 1) ∧ ´ind < length ´M}. ´ind :=
      ´ind + 1
      OD

lemmas mul_modules:

      Mul_Redirect_Edge j n == .{´Mul_mut_init n ∧ Z (´Muts ! j)}.
      ⟨IF T (´Muts ! j)
          ∈ Reach
             ´E THEN ´E := ´E
                     [R (´Muts ! j) := (fst (´E ! R (´Muts ! j)), T (´Muts ! j))] FI,,
      ´Muts := ´Muts[j := (´Muts ! j)(| Z := False |)]⟩

      Mul_Color_Target j n == .{´Mul_mut_init n ∧ ¬ Z (´Muts ! j)}.
      ⟨´M := ´M[T (´Muts ! j) := Black],,
      ´Muts := ´Muts[j := (´Muts ! j)(| Z := True |)]⟩

      Mul_Blacken_Roots n == .{´Mul_Proper n}. ´ind := 0;;
      .{´Mul_Proper n ∧ ´ind = 0}.
      WHILE ´ind < length ´M
      INV .{´Mul_Proper n ∧
            (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧ ´ind ≤ length ´M}.
      DO .{´Mul_Proper n ∧
           (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧ ´ind < length ´M}.
      IF ´ind ∈ Roots
      THEN .{´Mul_Proper n ∧
             (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧
             ´ind < length ´M ∧ ´ind ∈ Roots}. ´M :=
           ´M[´ind := Black]
      FI;;
      .{´Mul_Proper n ∧
        (∀i<´ind + 1. i ∈ Roots --> ´M ! i = Black) ∧ ´ind < length ´M}. ´ind :=
      ´ind + 1
      OD

      Mul_Propagate_Black n ==
      .{´Mul_Proper n ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´M ∧
        ´bc ⊆ Blacks ´M ∧ (´Safe ∨ ´l ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)}. ´ind :=
      0;;
      .{´Mul_Proper n ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´M ∧
        Blacks ´M ⊆ Blacks ´M ∧
        ´bc ⊆ Blacks ´M ∧ (´Safe ∨ ´l ≤ ´Queue ∨ ´obc ⊂ Blacks ´M) ∧ ´ind = 0}.
      WHILE ´ind < length ´E
      INV .{´Mul_Proper n ∧
            Roots ⊆ Blacks ´M ∧
            ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´Mul_PBInv ∧ ´ind ≤ length ´E}.
      DO .{´Mul_Proper n ∧
           Roots ⊆ Blacks ´M ∧
           ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´Mul_PBInv ∧ ´ind < length ´E}.
      IF ´M ! fst (´E ! ´ind) = Black
      THEN .{´Mul_Proper n ∧
             Roots ⊆ Blacks ´M ∧
             ´obc ⊆ Blacks ´M ∧
             ´bc ⊆ Blacks ´M ∧
             ´Mul_PBInv ∧ ´M ! fst (´E ! ´ind) = Black ∧ ´ind < length ´E}. ´k :=
           snd (´E ! ´ind);;
      .{´Mul_Proper n ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´M ∧
        ´bc ⊆ Blacks ´M ∧
        (´Safe ∨
         ´obc ⊂ Blacks ´M ∨
         ´l < ´Queue ∨ (∀i<´ind. ¬ BtoW (´E ! i, ´M)) ∧ ´l ≤ ´Queue ∧ ´Mul_Auxk) ∧
        ´k < length ´M ∧ ´M ! fst (´E ! ´ind) = Black ∧ ´ind < length ´E}.
      ⟨´M := ´M[´k := Black],, ´ind := ´ind + 1⟩
      ELSE .{´Mul_Proper n ∧
             Roots ⊆ Blacks ´M ∧
             ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´Mul_PBInv ∧ ´ind < length ´E}.
      ⟨IF ´M ! fst (´E ! ´ind) ≠ Black THEN ´ind := ´ind + 1 FI⟩ FI
      OD

      Mul_Count n ==
      .{´Mul_Proper n ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´Ma ∧
        Blacks ´Ma ⊆ Blacks ´M ∧
        ´bc ⊆ Blacks ´M ∧
        length ´Ma = length ´M ∧
        (´Safe ∨ ´obc ⊂ Blacks ´Ma ∨ ´l < ´q ∧ (´q ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)) ∧
        ´q < n + 1 ∧ ´bc = {}}. ´ind :=
      0;;
      .{´Mul_Proper n ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´Ma ∧
        Blacks ´Ma ⊆ Blacks ´M ∧
        ´bc ⊆ Blacks ´M ∧
        length ´Ma = length ´M ∧
        (´Safe ∨ ´obc ⊂ Blacks ´Ma ∨ ´l < ´q ∧ (´q ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)) ∧
        ´q < n + 1 ∧ ´bc = {} ∧ ´ind = 0}.
      WHILE ´ind < length ´M
      INV .{´Mul_Proper n ∧
            Roots ⊆ Blacks ´M ∧
            ´obc ⊆ Blacks ´Ma ∧
            Blacks ´Ma ⊆ Blacks ´M ∧
            ´bc ⊆ Blacks ´M ∧
            length ´Ma = length ´M ∧
            ´Mul_CountInv ´ind ∧
            (´Safe ∨ ´obc ⊂ Blacks ´Ma ∨ ´l < ´q ∧ (´q ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)) ∧
            ´q < n + 1 ∧ ´ind ≤ length ´M}.
      DO .{´Mul_Proper n ∧
           Roots ⊆ Blacks ´M ∧
           ´obc ⊆ Blacks ´Ma ∧
           Blacks ´Ma ⊆ Blacks ´M ∧
           ´bc ⊆ Blacks ´M ∧
           length ´Ma = length ´M ∧
           ´Mul_CountInv ´ind ∧
           (´Safe ∨ ´obc ⊂ Blacks ´Ma ∨ ´l < ´q ∧ (´q ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)) ∧
           ´q < n + 1 ∧ ´ind < length ´M}.
      IF ´M ! ´ind = Black
      THEN .{´Mul_Proper n ∧
             Roots ⊆ Blacks ´M ∧
             ´obc ⊆ Blacks ´Ma ∧
             Blacks ´Ma ⊆ Blacks ´M ∧
             ´bc ⊆ Blacks ´M ∧
             length ´Ma = length ´M ∧
             ´Mul_CountInv ´ind ∧
             (´Safe ∨
              ´obc ⊂ Blacks ´Ma ∨ ´l < ´q ∧ (´q ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)) ∧
             ´q < n + 1 ∧ ´ind < length ´M ∧ ´M ! ´ind = Black}. ´bc :=
           insert ´ind ´bc
      FI;;
      .{´Mul_Proper n ∧
        Roots ⊆ Blacks ´M ∧
        ´obc ⊆ Blacks ´Ma ∧
        Blacks ´Ma ⊆ Blacks ´M ∧
        ´bc ⊆ Blacks ´M ∧
        length ´Ma = length ´M ∧
        ´Mul_CountInv (´ind + 1) ∧
        (´Safe ∨ ´obc ⊂ Blacks ´Ma ∨ ´l < ´q ∧ (´q ≤ ´Queue ∨ ´obc ⊂ Blacks ´M)) ∧
        ´q < n + 1 ∧ ´ind < length ´M}. ´ind :=
      ´ind + 1
      OD

      Mul_Append n == .{´Mul_Proper n ∧ Roots ⊆ Blacks ´M ∧ ´Safe}. ´ind := 0;;
      .{´Mul_Proper n ∧ Roots ⊆ Blacks ´M ∧ ´Safe ∧ ´ind = 0}.
      WHILE ´ind < length ´M
      INV .{´Mul_Proper n ∧ ´Mul_AppendInv ´ind ∧ ´ind ≤ length ´M}.
      DO .{´Mul_Proper n ∧ ´Mul_AppendInv ´ind ∧ ´ind < length ´M}.
      IF ´M ! ´ind = Black
      THEN .{´Mul_Proper n ∧
             ´Mul_AppendInv ´ind ∧ ´ind < length ´M ∧ ´M ! ´ind = Black}. ´M :=
           ´M[´ind := White]
      ELSE .{´Mul_Proper n ∧
             ´Mul_AppendInv ´ind ∧ ´ind < length ´M ∧ ´ind ∉ Reach ´E}. ´E :=
           Append_to_free (´ind, ´E)
      FI;;
      .{´Mul_Proper n ∧ ´Mul_AppendInv (´ind + 1) ∧ ´ind < length ´M}. ´ind :=
      ´ind + 1
      OD

lemma Mul_Collector:

      \<turnstile> Mul_Collector n
         .{False}.

### Interference Freedom

lemma le_length_filter_update:

      (¬ P (list ! i) ∨ P j) ∧ i < length list
      ==> length (filter P list) ≤ length (filter P (list[i := j]))

lemma less_length_filter_update:

      P j ∧ ¬ P (list ! i) ∧ i < length list
      ==> length (filter P list) < length (filter P (list[i := j]))

lemma Mul_interfree_Blacken_Roots_Redirect_Edge:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Blacken_Roots n), {}, Some (Mul_Redirect_Edge j n))

lemma Mul_interfree_Redirect_Edge_Blacken_Roots:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Blacken_Roots n))

lemma Mul_interfree_Blacken_Roots_Color_Target:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Blacken_Roots n), {}, Some (Mul_Color_Target j n))

lemma Mul_interfree_Color_Target_Blacken_Roots:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Blacken_Roots n))

lemma Mul_interfree_Propagate_Black_Redirect_Edge:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux
           (Some (Mul_Propagate_Black n), {}, Some (Mul_Redirect_Edge j n))

lemma Mul_interfree_Redirect_Edge_Propagate_Black:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux
           (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Propagate_Black n))

lemma Mul_interfree_Propagate_Black_Color_Target:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux
           (Some (Mul_Propagate_Black n), {}, Some (Mul_Color_Target j n))

lemma Mul_interfree_Color_Target_Propagate_Black:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux
           (Some (Mul_Color_Target j n), {}, Some (Mul_Propagate_Black n))

lemma Mul_interfree_Count_Redirect_Edge:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Count n), {}, Some (Mul_Redirect_Edge j n))

lemma Mul_interfree_Redirect_Edge_Count:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Count n))

lemma Mul_interfree_Count_Color_Target:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Count n), {}, Some (Mul_Color_Target j n))

lemma Mul_interfree_Color_Target_Count:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Count n))

lemma Mul_interfree_Append_Redirect_Edge:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Append n), {}, Some (Mul_Redirect_Edge j n))

lemma Mul_interfree_Redirect_Edge_Append:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Append n))

lemma Mul_interfree_Append_Color_Target:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Append n), {}, Some (Mul_Color_Target j n))

lemma Mul_interfree_Color_Target_Append:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Append n))

#### Interference freedom Collector-Mutator

lemmas mul_collector_mutator_interfree:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Blacken_Roots n), {}, Some (Mul_Redirect_Edge j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Blacken_Roots n), {}, Some (Mul_Color_Target j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux
           (Some (Mul_Propagate_Black n), {}, Some (Mul_Redirect_Edge j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux
           (Some (Mul_Propagate_Black n), {}, Some (Mul_Color_Target j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Count n), {}, Some (Mul_Redirect_Edge j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Count n), {}, Some (Mul_Color_Target j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Append n), {}, Some (Mul_Redirect_Edge j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Append n), {}, Some (Mul_Color_Target j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Blacken_Roots n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Blacken_Roots n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux
           (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Propagate_Black n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux
           (Some (Mul_Color_Target j n), {}, Some (Mul_Propagate_Black n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Count n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Count n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Append n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Append n))

lemmas mul_collector_mutator_interfree:

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Blacken_Roots n), {}, Some (Mul_Redirect_Edge j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Blacken_Roots n), {}, Some (Mul_Color_Target j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux
           (Some (Mul_Propagate_Black n), {}, Some (Mul_Redirect_Edge j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux
           (Some (Mul_Propagate_Black n), {}, Some (Mul_Color_Target j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Count n), {}, Some (Mul_Redirect_Edge j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Count n), {}, Some (Mul_Color_Target j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Append n), {}, Some (Mul_Redirect_Edge j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Append n), {}, Some (Mul_Color_Target j n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Blacken_Roots n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Blacken_Roots n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux
           (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Propagate_Black n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux
           (Some (Mul_Color_Target j n), {}, Some (Mul_Propagate_Black n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Count n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Count n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Append n))

      [| 0 ≤ j; j < n |]
      ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Append n))

lemma Mul_interfree_Collector_Mutator:

      j < n ==> interfree_aux (Some (Mul_Collector n), {}, Some (Mul_Mutator j n))

#### Interference freedom Mutator-Collector

lemma Mul_interfree_Mutator_Collector:

      j < n ==> interfree_aux (Some (Mul_Mutator j n), {}, Some (Mul_Collector n))

#### The Multi-Mutator Garbage Collection Algorithm

lemma Mul_Gar_Coll:

      \<parallel>- .{´Mul_Proper n ∧ ´Mul_mut_init n ∧ (∀i<n. Z (´Muts ! i))}.
         COBEGIN
         Mul_Collector n
         .{False}.
         \<parallel>
         SCHEME [0 ≤ j < n] Mul_Mutator j n
          .{False}.
         COEND
         .{False}.