Theory BSPTaxonomy

theory BSPTaxonomy
imports "../../SystemSpecification/EventSystems"
  "../../SecuritySpecification/BasicSecurityPredicates"
begin

locale BSPTaxonomyDifferentCorrections =
fixes ES :: "'e ES_rec"
and 𝒱 :: "'e V_rec"

assumes validES: "ES_valid ES"
and VIsViewOnE: "isViewOn 𝒱 E⇘ES⇙"

locale BSPTaxonomyDifferentViews =
fixes ES :: "'e ES_rec"
and 𝒱⇩1 :: "'e V_rec"
and 𝒱⇩2 :: "'e V_rec"

assumes validES: "ES_valid ES"
and 𝒱⇩1IsViewOnE: "isViewOn 𝒱⇩1 E⇘ES⇙" 
and 𝒱⇩2IsViewOnE: "isViewOn 𝒱⇩2 E⇘ES⇙"

locale BSPTaxonomyDifferentViewsFirstDim= BSPTaxonomyDifferentViews +
assumes V2_subset_V1: "V⇘𝒱⇩2⇙ ⊆ V⇘𝒱⇩1⇙"  
and     N2_supset_N1: "N⇘𝒱⇩2⇙ ⊇ N⇘𝒱⇩1⇙"
and     C2_subset_C1: "C⇘𝒱⇩2⇙ ⊆ C⇘𝒱⇩1⇙"

sublocale  BSPTaxonomyDifferentViewsFirstDim ⊆ BSPTaxonomyDifferentViews
by (unfold_locales)

locale BSPTaxonomyDifferentViewsSecondDim= BSPTaxonomyDifferentViews +
assumes V2_subset_V1: "V⇘𝒱⇩2⇙ ⊆ V⇘𝒱⇩1⇙"  
and     N2_supset_N1: "N⇘𝒱⇩2⇙ ⊇ N⇘𝒱⇩1⇙"
and     C2_equals_C1: "C⇘𝒱⇩2⇙ = C⇘𝒱⇩1⇙"

sublocale  BSPTaxonomyDifferentViewsSecondDim ⊆ BSPTaxonomyDifferentViews
by (unfold_locales)

(* body of BSPTaxonomy *)
context BSPTaxonomyDifferentCorrections
begin

(*lemma taken from lemma 3.5.1 from Heiko Mantel's dissertation*)
lemma SR_implies_R: 
"SR 𝒱 Tr⇘ES⇙ ⟹ R 𝒱 Tr⇘ES⇙"
proof -
  assume SR: "SR 𝒱 Tr⇘ES⇙"
  {
    fix τ
    assume "τ ∈ Tr⇘ES⇙"
    with SR  have "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ Tr⇘ES⇙" 
      unfolding SR_def by auto 
    hence "∃ τ'. τ' ∈ Tr⇘ES⇙ ∧ τ' ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙ ∧ τ' ↿ C⇘𝒱⇙ = []"
    proof -
      assume tau_V_N_is_trace: "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ Tr⇘ES⇙"
      show "∃ τ'. τ' ∈ Tr⇘ES⇙ ∧ τ' ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙ ∧ τ' ↿ C⇘𝒱⇙ = []"
      proof
        let  ?τ'= "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
        have "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙" 
          by (simp add: projection_subset_elim) 
        moreover
        from  VIsViewOnE have "VC_disjoint 𝒱 ∧ NC_disjoint 𝒱" 
          unfolding isViewOn_def V_valid_def
          by auto
        then have "(V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∩ C⇘𝒱⇙ = {}" 
          by (simp add: NC_disjoint_def VC_disjoint_def inf_sup_distrib2) 
        then have "?τ' ↿ C⇘𝒱⇙ = []" 
          by (simp add: disjoint_projection)
        ultimately
        show "?τ' ∈ Tr⇘ES⇙ ∧ ?τ' ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙ ∧ ?τ' ↿ C⇘𝒱⇙ = []" 
          using  tau_V_N_is_trace  by auto 
      qed  
    qed
  }
  thus ?thesis
    unfolding SR_def R_def by auto
qed

(* lemma taken from lemma 3.5.1 from Heiko Mantel's dissertation *)
lemma SD_implies_BSD :
"(SD 𝒱 Tr⇘ES⇙) ⟹ BSD 𝒱 Tr⇘ES⇙ "
proof -
  assume SD:  "SD 𝒱 Tr⇘ES⇙"
  { 
    fix α β c 
    assume "c ∈ C⇘𝒱⇙"
      and  "β @ c # α ∈ Tr⇘ES⇙" 
      and  alpha_C_empty: "α ↿ C⇘𝒱⇙ = []" 
    with SD have "β @ α ∈ Tr⇘ES⇙"
      unfolding SD_def by auto
    hence "∃α'. β @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []"
      using alpha_C_empty  
      by auto
   }
   thus ?thesis
     unfolding SD_def BSD_def by auto
qed

(* lemma taken from lemma 3.5.1 from Heiko Mantel's dissertation *)
lemma BSD_implies_D: 
"BSD 𝒱 Tr⇘ES⇙ ⟹ D 𝒱 Tr⇘ES⇙"
proof - 
  assume BSD: "BSD 𝒱 Tr⇘ES⇙"
  
  {
    fix α β c
    assume "α ↿ C⇘𝒱⇙ = []"
      and "c ∈ C⇘𝒱⇙"
      and "β @ [c] @ α ∈ Tr⇘ES⇙"
    with BSD obtain α' 
      where "β @ α' ∈ Tr⇘ES⇙"
      and "α' ↿ V⇘𝒱⇙ = α ↿ V 𝒱"
      and  "α' ↿ C⇘𝒱⇙ = []"
      by (simp add: BSD_def, auto)
    hence "(∃α' β'.
      (β' @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []) ∧
      β' ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙))"
      by auto
  }
  thus ?thesis
    unfolding BSD_def D_def
    by auto
qed

(* lemma taken from lemma 3.5.1 from Heiko Mantel's dissertation *)
lemma SD_implies_SR: 
"SD 𝒱 Tr⇘ES⇙ ⟹ SR 𝒱 Tr⇘ES⇙"
unfolding SR_def
proof
  fix τ 

  assume SD: "SD 𝒱 Tr⇘ES⇙"
  assume τ_trace: "τ ∈ Tr⇘ES⇙"
  
  {
    fix  n 

      (* show via induction over length (τ ↿ C⇘𝒱⇙) that SR holds *)
    have SR_via_length: " ⟦ τ ∈ Tr⇘ES⇙; n = length (τ ↿ C⇘𝒱⇙) ⟧ 
      ⟹ ∃τ' ∈ Tr⇘ES⇙. τ' ↿ C⇘𝒱⇙ = [] ∧ τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
    proof (induct n arbitrary: τ)
      case 0 
      note τ_in_Tr = ‹τ ∈ Tr⇘ES⇙›
        and ‹0 = length (τ ↿ C⇘𝒱⇙)›
      hence "τ ↿ C⇘𝒱⇙ = []" 
        by simp
      with τ_in_Tr show ?case 
        by auto
    next
      case (Suc n)
      from projection_split_last[OF Suc(3)] obtain β c α
        where c_in_C: "c ∈ C⇘𝒱⇙"
        and τ_is_βcα: "τ = β @ [c] @ α"
        and α_no_c: "α ↿ C⇘𝒱⇙ = []"
        and βα_contains_n_cs: "n = length ((β @ α) ↿ C⇘𝒱⇙)"
      by auto
      with Suc(2) have βcα_in_Tr: "β @ [c] @ α ∈ Tr⇘ES⇙"
        by auto
      
      with SD c_in_C βcα_in_Tr α_no_c obtain β' α' 
        where β'α'_in_Tr: "(β' @ α') ∈ Tr⇘ES⇙" 
        and α'_V_is_α_V: "α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
        and α'_no_c: "α' ↿ C⇘𝒱⇙ = []" 
        and β'_VC_is_β_VC: "β' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙) = β ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙)"
        unfolding SD_def
        by blast
       
      have "(β' @ α') ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
      proof - 
        from β'_VC_is_β_VC have  "β' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = β ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
          by (rule projection_subset_eq_from_superset_eq)
        with α'_V_is_α_V have "(β' @ α') ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = (β @ α) ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
          by (simp add: projection_def)
        moreover
        with  VIsViewOnE c_in_C have "c ∉ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
          by (simp add: isViewOn_def V_valid_def VC_disjoint_def NC_disjoint_def, auto)
        hence "(β @ α) ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = (β @ [c] @ α) ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
          by (simp add: projection_def)
        moreover note τ_is_βcα
        ultimately show ?thesis
          by auto
      qed
      moreover 
      have "n = length ((β' @ α') ↿ C⇘𝒱⇙)"
      proof -
        have  "β' ↿ C⇘𝒱⇙ = β ↿ C⇘𝒱⇙"
        proof -
          have "V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙ = C⇘𝒱⇙ ∪ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
            by auto
          with β'_VC_is_β_VC have "β' ↿ (C⇘𝒱⇙ ∪ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)) = β ↿ (C⇘𝒱⇙ ∪ (V⇘𝒱⇙ ∪ N⇘𝒱⇙))"
            by auto
          thus ?thesis
            by (rule projection_subset_eq_from_superset_eq)
        qed
        with α'_no_c α_no_c have "(β' @ α') ↿ C⇘𝒱⇙ = (β @ α) ↿ C⇘𝒱⇙"
          by (simp add: projection_def)
        with βα_contains_n_cs show ?thesis
          by auto
      qed
      with Suc.hyps β'α'_in_Tr obtain τ' 
        where  "τ' ∈ Tr⇘ES⇙" 
        and "τ' ↿ C⇘𝒱⇙ = []" 
        and "τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = (β' @ α') ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
        by auto
      ultimately show ?case
        by auto
    qed 
  }
  
  hence "τ ∈ Tr⇘ES⇙ ⟹ ∃τ'. τ'∈Tr⇘ES⇙ ∧ τ' ↿ C⇘𝒱⇙ = [] ∧ τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)" 
    by auto

  from this τ_trace obtain τ' where
        τ'_trace : "τ'∈Tr⇘ES⇙"
    and τ'_no_C  : "τ' ↿ C⇘𝒱⇙ = []"
    and τ'_τ_rel : "τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)" 
  by auto

  from τ'_no_C have "τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙) = τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)" 
    by (auto simp add: projection_on_union)

  with  VIsViewOnE have τ'_E_eq_VN: "τ' ↿ E⇘ES⇙ = τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)" 
    by (auto simp add: isViewOn_def)

  from validES τ'_trace have "(set τ') ⊆ E⇘ES⇙" 
    by (auto simp add: ES_valid_def traces_contain_events_def)
  hence "τ' ↿ E⇘ES⇙ = τ'" by (simp add: list_subset_iff_projection_neutral)
  with τ'_E_eq_VN have "τ' = τ' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)" by auto
  with τ'_τ_rel have "τ' = τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)" by auto
  with τ'_trace show "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ Tr⇘ES⇙" by auto
qed

(* lemma taken from lemma 3.5.1 from Heiko Mantel's dissertation *)
lemma D_implies_R: 
"D 𝒱 Tr⇘ES⇙ ⟹ R 𝒱 Tr⇘ES⇙"
proof -
  assume D: "D 𝒱 Tr⇘ES⇙"  
  {
    fix τ n 

      (* show via induction over length (τ ↿ C⇘𝒱⇙) that R holds *)
    have R_via_length: " ⟦ τ ∈ Tr⇘ES⇙; n = length (τ ↿ C⇘𝒱⇙) ⟧
                          ⟹ ∃τ' ∈ Tr⇘ES⇙. τ' ↿ C⇘𝒱⇙ = [] ∧ τ' ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙"
    proof (induct n arbitrary: τ)
      case 0 
      note τ_in_Tr = ‹τ ∈ Tr⇘ES⇙›
        and ‹0 = length (τ ↿ C⇘𝒱⇙)›
      hence "τ ↿ C⇘𝒱⇙ = []" 
        by simp
      with τ_in_Tr show ?case 
        by auto
    next
      case (Suc n)
      from projection_split_last[OF Suc(3)] obtain β c α
        where c_in_C: "c ∈ C⇘𝒱⇙"
        and τ_is_βcα: "τ = β @ [c] @ α"
        and α_no_c: "α ↿ C⇘𝒱⇙ = []"
        and βα_contains_n_cs: "n = length ((β @ α) ↿ C⇘𝒱⇙)"
      by auto
      with Suc(2) have βcα_in_Tr: "β @ [c] @ α ∈ Tr⇘ES⇙"
        by auto
      
      with D c_in_C βcα_in_Tr α_no_c obtain β' α' 
        where β'α'_in_Tr: "(β' @ α') ∈ Tr⇘ES⇙" 
        and α'_V_is_α_V: "α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙"
        and α'_no_c: "α' ↿ C⇘𝒱⇙ = []" 
        and β'_VC_is_β_VC: "β' ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙)"
        unfolding D_def 
        by blast

      have "(β' @ α') ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙"
      proof - 
        from β'_VC_is_β_VC have  "β' ↿ V⇘𝒱⇙ = β ↿ V⇘𝒱⇙"
          by (rule projection_subset_eq_from_superset_eq)
        with α'_V_is_α_V have "(β' @ α') ↿ V⇘𝒱⇙ = (β @ α) ↿ V⇘𝒱⇙"
          by (simp add: projection_def)
        moreover
        with  VIsViewOnE c_in_C have "c ∉ V⇘𝒱⇙"
          by (simp add: isViewOn_def V_valid_def VC_disjoint_def, auto)
        hence "(β @ α) ↿ V⇘𝒱⇙ = (β @ [c] @ α) ↿ V⇘𝒱⇙"
          by (simp add: projection_def)
        moreover note τ_is_βcα
        ultimately show ?thesis
          by auto
      qed
      moreover 
      have "n = length ((β' @ α') ↿ C⇘𝒱⇙)"
      proof -
        have  "β' ↿ C⇘𝒱⇙ = β ↿ C⇘𝒱⇙"
        proof -
          have "V⇘𝒱⇙ ∪ C⇘𝒱⇙ = C⇘𝒱⇙ ∪ V⇘𝒱⇙"
            by auto
          with β'_VC_is_β_VC have "β' ↿ (C⇘𝒱⇙ ∪ V⇘𝒱⇙) = β ↿ (C⇘𝒱⇙ ∪ V⇘𝒱⇙)"
            by auto
          thus ?thesis
            by (rule projection_subset_eq_from_superset_eq)
        qed
        with α'_no_c α_no_c have "(β' @ α') ↿ C⇘𝒱⇙ = (β @ α) ↿ C⇘𝒱⇙"
          by (simp add: projection_def)
        with βα_contains_n_cs show ?thesis
          by auto
      qed
      with Suc.hyps β'α'_in_Tr obtain τ' 
        where  "τ' ∈ Tr⇘ES⇙" 
        and "τ' ↿ C⇘𝒱⇙ = []" 
        and "τ' ↿ V⇘𝒱⇙ = (β' @ α') ↿ V⇘𝒱⇙"
        by auto
      ultimately show ?case
        by auto
    qed 
  }
  thus ?thesis
    by (simp add: R_def)
qed

(* Theorem 3.5.6.1 from Heiko Mantel's dissertation *)
lemma SR_implies_R_for_modified_view :
"⟦SR 𝒱 Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈⟧ ⟹ R 𝒱' Tr⇘ES⇙" 
proof -
  assume "SR 𝒱 Tr⇘ES⇙"
     and "𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈"
   {
     from ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› VIsViewOnE 
     have V'IsViewOnE: "isViewOn 𝒱' E⇘ES⇙ " 
       unfolding isViewOn_def V_valid_def VC_disjoint_def NC_disjoint_def VN_disjoint_def by auto
    fix τ
    assume "τ ∈ Tr⇘ES⇙"
    with ‹SR 𝒱 Tr⇘ES⇙› have "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ Tr⇘ES⇙"
      unfolding SR_def by auto
    
    let ?τ'="τ ↿V⇘𝒱'⇙"
    
    from ‹τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ Tr⇘ES⇙› have "?τ' ∈ Tr⇘ES⇙" 
      using ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› by simp
    moreover   
    from V'IsViewOnE have "?τ'↿C⇘𝒱'⇙=[]"
      using disjoint_projection  
      unfolding isViewOn_def V_valid_def VC_disjoint_def by auto
    moreover  
    have "?τ'↿V⇘𝒱'⇙ = τ↿V⇘𝒱'⇙"
      by (simp add: projection_subset_elim)
    ultimately
    have "∃τ'∈Tr⇘ES⇙. τ' ↿ C⇘𝒱'⇙ = [] ∧ τ' ↿ V⇘𝒱'⇙ = τ ↿ V⇘𝒱'⇙"
      by auto
   }
  with ‹SR 𝒱 Tr⇘ES⇙› show ?thesis 
    unfolding R_def using ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› by auto 
qed   

lemma R_implies_SR_for_modified_view : 
"⟦R 𝒱' Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈⟧ ⟹ SR 𝒱 Tr⇘ES⇙"
proof -
  assume "R 𝒱' Tr⇘ES⇙"
     and "𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈"
  {
    fix τ
    assume "τ ∈ Tr⇘ES⇙"
    from ‹R 𝒱' Tr⇘ES⇙› ‹τ ∈ Tr⇘ES⇙›  obtain τ' where "τ' ∈ Tr⇘ES⇙"
                                        and "τ' ↿ C⇘𝒱'⇙ = []" 
                                        and "τ' ↿ V⇘𝒱'⇙ = τ ↿ V⇘𝒱'⇙"
                                        unfolding R_def by auto
    from VIsViewOnE ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›  have "isViewOn  𝒱' E⇘ES⇙" 
      unfolding isViewOn_def V_valid_def  VN_disjoint_def VC_disjoint_def NC_disjoint_def                                   
      by auto

    from ‹τ' ↿ V⇘𝒱'⇙ = τ ↿ V⇘𝒱'⇙›  ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› 
    have "τ' ↿ (V⇘𝒱'⇙ ∪ N⇘𝒱'⇙) = τ ↿ (V⇘𝒱'⇙ ∪ N⇘𝒱'⇙)" 
      by simp
    
    from ‹τ' ↿ C⇘𝒱'⇙ = []› have "τ' =τ' ↿ (V⇘𝒱'⇙ ∪ N⇘𝒱'⇙)"
      using validES ‹τ' ∈ Tr⇘ES⇙› ‹isViewOn 𝒱' E⇘ES⇙› 
      unfolding projection_def ES_valid_def isViewOn_def traces_contain_events_def
      by (metis UnE filter_True filter_empty_conv)
    hence  "τ' =τ ↿ (V⇘𝒱'⇙ ∪ N⇘𝒱'⇙)" 
      using ‹τ' ↿ (V⇘𝒱'⇙ ∪ N⇘𝒱'⇙) = τ ↿ (V⇘𝒱'⇙ ∪ N⇘𝒱'⇙)›
      by simp                 
    with ‹τ' ∈ Tr⇘ES⇙› have "τ ↿ (V⇘𝒱'⇙ ∪ N⇘𝒱'⇙) ∈ Tr⇘ES⇙" 
      by auto
  } 
  thus ?thesis 
    unfolding SR_def using ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
    by simp
qed

(* Theorem 3.5.6.2 from Heiko Mantel's dissertation *)
lemma SD_implies_BSD_for_modified_view :
"⟦SD 𝒱 Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈⟧ ⟹ BSD 𝒱' Tr⇘ES⇙" 
proof -
  assume "SD 𝒱 Tr⇘ES⇙"
     and "𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈"
   {
    fix α β c
    assume "c ∈ C⇘𝒱'⇙"
       and "β @ [c] @ α ∈ Tr⇘ES⇙"
       and "α↿C⇘𝒱'⇙ = []"
    
    from ‹c ∈ C⇘𝒱'⇙›  ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
    have "c ∈ C⇘𝒱⇙" 
      by auto     
    from ‹α↿C⇘𝒱'⇙ = []› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› 
    have "α↿C⇘𝒱⇙ = []" 
      by auto

    from ‹c ∈ C⇘𝒱⇙› ‹β @ [c] @ α ∈ Tr⇘ES⇙› ‹α↿C⇘𝒱⇙ = []› 
    have "β @ α ∈ Tr⇘ES⇙" using ‹SD 𝒱 Tr⇘ES⇙›
      unfolding SD_def by auto
    hence  "∃α'. β @ α' ∈ Tr⇘ES⇙ ∧  α' ↿ V⇘𝒱'⇙ = α ↿ V⇘𝒱'⇙  ∧ α' ↿ C⇘𝒱'⇙ = [] " 
      using ‹α ↿ C⇘𝒱'⇙ = []› by blast
   }
  with ‹SD 𝒱 Tr⇘ES⇙› show ?thesis 
    unfolding BSD_def using ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› by auto 
qed   

lemma BSD_implies_SD_for_modified_view : 
"⟦BSD 𝒱' Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈⟧ ⟹ SD 𝒱 Tr⇘ES⇙"
  unfolding SD_def
  proof(clarsimp)
  fix α β c
  assume BSD_view' : "BSD ⦇V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N = {} , C = C⇘𝒱⇙⦈ Tr⇘ES⇙"
  assume alpha_no_C_view : "α ↿ C⇘𝒱⇙ = []"
  assume c_C_view : "c ∈ C⇘𝒱⇙"
  assume beta_c_alpha_is_trace : "β @ c # α ∈ Tr⇘ES⇙"
  
  from BSD_view' alpha_no_C_view c_C_view beta_c_alpha_is_trace 
  obtain α' 
    where beta_alpha'_is_trace: "β @ α'∈(Tr⇘ES⇙)" 
      and alpha_alpha': "α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
      and alpha'_no_C_view : "α' ↿ C⇘𝒱⇙ = []"
    by (auto simp add: BSD_def)

  from beta_c_alpha_is_trace validES
  have alpha_consists_of_events: "set α ⊆ E⇘ES⇙" 
      by (auto simp add: ES_valid_def traces_contain_events_def)

  from alpha_no_C_view have "α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙) = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
    by (rule projection_on_union)
  with VIsViewOnE  have alpha_on_ES : "α ↿ E⇘ES⇙ = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)" 
    unfolding isViewOn_def by simp

  from alpha_consists_of_events VIsViewOnE have "α ↿ E⇘ES⇙ = α"
    by (simp add: list_subset_iff_projection_neutral)
  
  with alpha_on_ES have α_eq: "α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α" by auto

  from beta_alpha'_is_trace validES
  have alpha'_consists_of_events: "set α' ⊆ E⇘ES⇙" 
    by (auto simp add: ES_valid_def traces_contain_events_def)

  from alpha'_no_C_view have "α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙) = α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
    by (rule projection_on_union)
  with VIsViewOnE have alpha'_on_ES : "α' ↿ E⇘ES⇙ = α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
    unfolding isViewOn_def by (simp)

  from alpha'_consists_of_events VIsViewOnE have "α' ↿ E⇘ES⇙ = α'"
    by (simp add: list_subset_iff_projection_neutral)
  
  with alpha'_on_ES have α'_eq: "α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α'" by auto


  from alpha_alpha' α_eq α'_eq have "α = α'" by auto
    
  with beta_alpha'_is_trace show "β @ α ∈ Tr⇘ES⇙" by auto
qed


(* lemma taken from lemma 3.5.4 from Heiko Mantel's dissertation*)
lemma SD_implies_FCD: 
"(SD 𝒱 Tr⇘ES⇙) ⟹ FCD Γ 𝒱 Tr⇘ES⇙"
proof -    
   assume SD: "SD 𝒱 Tr⇘ES⇙"
    { 
    fix α β c v
    assume "c ∈ C⇘𝒱⇙  ∩ Υ⇘Γ⇙"
      and  "v ∈ V⇘𝒱⇙  ∩ ∇⇘Γ⇙"
      and alpha_C_empty: "α ↿ C⇘𝒱⇙ = []"
      and  "β @ [c, v] @ α ∈ Tr⇘ES⇙"
    moreover
    with VIsViewOnE  have "(v # α) ↿ C⇘𝒱⇙ = []" 
      unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto
    ultimately
    have "β @ (v # α) ∈ Tr⇘ES⇙" 
      using SD unfolding SD_def by auto
    with alpha_C_empty  
    have "∃α'. ∃δ'. (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ δ' @ [v] @ α') ∈  Tr⇘ES⇙  
            ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = [])" 
      by (metis append.simps(1) append.simps(2) bot_least list.set(1))
  }    
  thus ?thesis 
    unfolding SD_def FCD_def by auto
qed



(* lemma taken from lemma 3.5.9 from Heiko Mantel's dissertation *)
lemma SI_implies_BSI :
"(SI 𝒱 Tr⇘ES⇙) ⟹ BSI 𝒱 Tr⇘ES⇙ "
proof -
  assume SI: "SI 𝒱 Tr⇘ES⇙"
  { 
    fix α β c 
    assume "c ∈ C⇘𝒱⇙"
      and  "β @  α ∈ Tr⇘ES⇙" 
      and alpha_C_empty: "α ↿ C⇘𝒱⇙ = []" 
    with SI have "β @ c # α ∈ Tr⇘ES⇙" 
      unfolding SI_def by auto
    hence  "∃α'. β @ c # α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []" 
      using alpha_C_empty  by auto
  }
  thus ?thesis 
    unfolding SI_def BSI_def by auto
qed

(* lemma taken from lemma 3.5.9 from Heiko Mantel's dissertation *)
lemma BSI_implies_I: 
"(BSI 𝒱 Tr⇘ES⇙) ⟹ (I 𝒱 Tr⇘ES⇙)"
proof -
  assume BSI: "BSI 𝒱 Tr⇘ES⇙"

  {
    fix α β c
    assume "c ∈ C⇘𝒱⇙"
      and "β @ α ∈ Tr⇘ES⇙"
      and "α ↿ C⇘𝒱⇙ = []"
    with BSI obtain α' 
      where "β @ [c] @ α' ∈ Tr⇘ES⇙"
      and "α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙"
      and  "α' ↿ C⇘𝒱⇙ = []"
      unfolding BSI_def
      by blast
    hence 
      "(∃α' β'. (β' @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []) ∧
                  β' ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙))"
      by auto
  }
  thus ?thesis unfolding BSI_def I_def
    by auto
qed

(* lemma taken from lemma 3.5.9 from Heiko Mantel's dissertation *)
lemma SIA_implies_BSIA: 
"(SIA ρ 𝒱 Tr⇘ES⇙) ⟹ (BSIA ρ 𝒱 Tr⇘ES⇙)"
proof -
  assume SIA: "SIA ρ 𝒱 Tr⇘ES⇙"
  {
    fix α β c
    assume "c ∈ C⇘𝒱⇙"
      and "β @ α ∈ Tr⇘ES⇙"
      and alpha_C_empty: "α ↿ C⇘𝒱⇙ = []"
      and "(Adm 𝒱 ρ Tr⇘ES⇙ β c)"
    with SIA obtain "β @ c # α ∈ Tr⇘ES⇙"
      unfolding SIA_def by auto
    hence "∃ α'. β @ c # α' ∈ Tr⇘ES⇙ ∧ α'↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []"  
      using  alpha_C_empty  by auto
  }
  thus ?thesis
    unfolding SIA_def BSIA_def by auto
qed

(* lemma taken from lemma 3.5.9 from Heiko Mantel's dissertation *)
lemma BSIA_implies_IA: 
"(BSIA ρ 𝒱 Tr⇘ES⇙) ⟹ (IA ρ 𝒱 Tr⇘ES⇙)"
proof -
  assume BSIA: "BSIA ρ 𝒱 Tr⇘ES⇙"

  {
    fix α β c
    assume "c ∈ C⇘𝒱⇙"
      and "β @ α ∈ Tr⇘ES⇙"
      and "α ↿ C⇘𝒱⇙ = []"
      and "(Adm 𝒱 ρ Tr⇘ES⇙ β c)"
    with BSIA obtain α' 
      where "β @ [c] @ α' ∈ Tr⇘ES⇙"
      and "α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙"
      and  "α' ↿ C⇘𝒱⇙ = []"
      unfolding BSIA_def
      by blast
    hence "(∃α' β'.
      (β' @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []) ∧
      β' ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β ↿ (V⇘𝒱⇙ ∪ C⇘𝒱⇙))"
      by auto
  }
  thus ?thesis 
    unfolding BSIA_def IA_def by auto
qed

(* lemma taken from lemma 3.5.9 from Heiko Mantel's dissertation *)
lemma SI_implies_SIA: 
"SI 𝒱 Tr⇘ES⇙ ⟹ SIA ρ 𝒱 Tr⇘ES⇙" 
proof -
  assume SI: "SI 𝒱 Tr⇘ES⇙"
  {
    fix α β c
    assume "c ∈ C⇘𝒱⇙"
      and  "β @ α ∈ Tr⇘ES⇙"
      and  "α ↿ C⇘𝒱⇙ = []"
      and  "Adm 𝒱 ρ Tr⇘ES⇙ β c"
    with SI have "β @ (c # α) ∈ Tr⇘ES⇙"
      unfolding SI_def by auto  
  }
  thus ?thesis unfolding SI_def SIA_def by auto  
qed

(* lemma taken from lemma 3.5.9 from Heiko Mantel's dissertation *)
lemma BSI_implies_BSIA: 
"BSI 𝒱 Tr⇘ES⇙ ⟹ BSIA ρ 𝒱 Tr⇘ES⇙" 
proof -
  assume BSI: "BSI 𝒱 Tr⇘ES⇙"
  {
    fix α β c
    assume "c ∈ C⇘𝒱⇙"
      and  "β @ α ∈ Tr⇘ES⇙"
      and  "α ↿ C⇘𝒱⇙ = []"
      and  "Adm 𝒱 ρ Tr⇘ES⇙ β c"
    with BSI have "∃ α'. β @ (c # α') ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙  ∧ α' ↿ C⇘𝒱⇙ = []" 
      unfolding BSI_def by auto  
  }
  thus ?thesis
    unfolding BSI_def BSIA_def by auto  
qed

(* lemma taken from lemma 3.5.9 from Heiko Mantel's dissertation *)
lemma I_implies_IA: 
"I 𝒱 Tr⇘ES⇙ ⟹ IA ρ 𝒱 Tr⇘ES⇙" 
proof -
  assume I: "I 𝒱 Tr⇘ES⇙"
  {
    fix α β c
    assume "c ∈ C⇘𝒱⇙"
      and  "β @ α ∈ Tr⇘ES⇙"
      and  "α ↿ C⇘𝒱⇙ = []"
      and  "Adm 𝒱 ρ Tr⇘ES⇙ β c"
    with I have "∃ α' β'. β' @ (c # α') ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙  
                            ∧ α' ↿ C⇘𝒱⇙ = []  ∧ β' ↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β ↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) " 
      unfolding I_def by auto  
  }
  thus ?thesis
    unfolding I_def IA_def by auto  
qed

(* Theorem 3.5.15.1 from Heiko Mantel's dissertation *)
lemma SI_implies_BSI_for_modified_view :
"⟦SI 𝒱 Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈⟧ ⟹ BSI 𝒱' Tr⇘ES⇙" 
proof -
  assume "SI 𝒱 Tr⇘ES⇙"
     and "𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈"
   {
    fix α β c
    assume "c ∈ C⇘𝒱'⇙"
       and "β  @ α ∈ Tr⇘ES⇙"
       and "α↿C⇘𝒱'⇙ = []"
    
    from ‹c ∈ C⇘𝒱'⇙›  ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
    have "c ∈ C⇘𝒱⇙"
      by auto     
    from ‹α↿C⇘𝒱'⇙ = []› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› 
    have "α↿C⇘𝒱⇙ = []"
      by auto

    from ‹c ∈ C⇘𝒱⇙› ‹β  @ α ∈ Tr⇘ES⇙› ‹α↿C⇘𝒱⇙ = []› 
    have "β @ [c] @  α ∈ Tr⇘ES⇙" 
      using ‹SI 𝒱 Tr⇘ES⇙›  unfolding SI_def by auto
    hence  "∃α'. β @ [c] @  α' ∈ Tr⇘ES⇙ ∧  α' ↿ V⇘𝒱'⇙ = α ↿ V⇘𝒱'⇙  ∧ α' ↿ C⇘𝒱'⇙ = [] " 
      using ‹α ↿ C⇘𝒱'⇙ = []› 
      by blast
   }
  with ‹SI 𝒱 Tr⇘ES⇙› show ?thesis 
    unfolding BSI_def using ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› by auto 
qed 

lemma BSI_implies_SI_for_modified_view : 
"⟦BSI 𝒱' Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N = {} , C = C⇘𝒱⇙ ⦈⟧ ⟹ SI 𝒱 Tr⇘ES⇙"
  unfolding SI_def
  proof (clarsimp)
  fix α β c
  assume BSI_view' : "BSI ⦇V = V⇘𝒱⇙ ∪ N⇘𝒱⇙, N = {}, C = C⇘𝒱⇙⦈ Tr⇘ES⇙"
  assume alpha_no_C_view : "α ↿ C⇘𝒱⇙ = []"
  assume c_C_view : "c ∈ C⇘𝒱⇙"
  assume beta_alpha_is_trace : "β @ α ∈ Tr⇘ES⇙"

  from BSI_view' have "∀c∈C⇘𝒱⇙. β @ α ∈ Tr⇘ES⇙ ∧ α ↿ C⇘𝒱⇙ = [] 
    ⟶ (∃α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∧ α' ↿ C⇘𝒱⇙ = [])" 
    by (auto simp add: BSI_def)

  with beta_alpha_is_trace alpha_no_C_view have "∀c∈C⇘𝒱⇙.
        (∃α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∧ α' ↿ C⇘𝒱⇙ = [])" 
    by auto

  with this BSI_view' c_C_view obtain α'
    where beta_c_alpha'_is_trace: "β @ [c] @ α' ∈ Tr⇘ES⇙" 
      and alpha_alpha': "α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
      and alpha'_no_C_view : "α' ↿ C⇘𝒱⇙ = []"
    by auto

  from beta_alpha_is_trace validES
  have alpha_consists_of_events: "set α ⊆ E⇘ES⇙" 
    by (auto simp add: ES_valid_def traces_contain_events_def)

  from alpha_no_C_view have "α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙) = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
    by (rule projection_on_union)
  with VIsViewOnE have alpha_on_ES : "α ↿ E⇘ES⇙ = α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)" 
    unfolding isViewOn_def by (simp)

  from alpha_consists_of_events VIsViewOnE have "α ↿ E⇘ES⇙ = α"
    by (simp add: list_subset_iff_projection_neutral)
  
  with alpha_on_ES have α_eq: "α ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α" by auto
  
  from beta_c_alpha'_is_trace validES 
  have alpha'_consists_of_events: "set α' ⊆ E⇘ES⇙" 
    by (auto simp add: ES_valid_def traces_contain_events_def)

  from alpha'_no_C_view have "α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙) = α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)"
    by (rule projection_on_union)
  with VIsViewOnE have alpha'_on_ES : "α' ↿ E⇘ES⇙ = α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)" 
    unfolding isViewOn_def by (simp)

  from alpha'_consists_of_events VIsViewOnE have "α' ↿ E⇘ES⇙ = α'"
    by (simp add: list_subset_iff_projection_neutral)
  
  with alpha'_on_ES have α'_eq: "α' ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) = α'" by auto

  from alpha_alpha' α_eq α'_eq have "α = α'" by auto
    
  with beta_c_alpha'_is_trace show "β @ c # α ∈ Tr⇘ES⇙" by auto
qed


(* lemma taken from Theorem 3.5.15.2 from Heiko Mantel's dissertation *)
lemma SIA_implies_BSIA_for_modified_view :
"⟦SIA ρ 𝒱 Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈ ; ρ 𝒱 = ρ' 𝒱'⟧ ⟹ BSIA ρ' 𝒱' Tr⇘ES⇙" 
proof -
  assume "SIA ρ 𝒱 Tr⇘ES⇙"
     and "𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈"
     and "ρ 𝒱 = ρ' 𝒱'"
   {
    fix α β c
    assume "c ∈ C⇘𝒱'⇙"
       and "β  @ α ∈ Tr⇘ES⇙"
       and "α↿C⇘𝒱'⇙ = []"
       and "Adm 𝒱' ρ' Tr⇘ES⇙ β c"
    
    from ‹c ∈ C⇘𝒱'⇙›  ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
    have "c ∈ C⇘𝒱⇙"
      by auto     
    from ‹α↿C⇘𝒱'⇙ = []› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› 
    have "α↿C⇘𝒱⇙ = []"
      by auto
    from  ‹Adm 𝒱' ρ' Tr⇘ES⇙ β c› ‹ρ 𝒱 = ρ' 𝒱'› 
    have "Adm 𝒱 ρ Tr⇘ES⇙ β c"
      by (simp add: Adm_def)

    from ‹c ∈ C⇘𝒱⇙› ‹β  @ α ∈ Tr⇘ES⇙› ‹α↿C⇘𝒱⇙ = []› ‹Adm 𝒱 ρ Tr⇘ES⇙ β c›
    have "β @ [c] @  α ∈ Tr⇘ES⇙" 
      using ‹SIA ρ 𝒱 Tr⇘ES⇙›  unfolding SIA_def by auto
    hence  "∃α'. β @ [c] @  α' ∈ Tr⇘ES⇙ ∧  α' ↿ V⇘𝒱'⇙ = α ↿ V⇘𝒱'⇙  ∧ α' ↿ C⇘𝒱'⇙ = [] " 
      using ‹α ↿ C⇘𝒱'⇙ = []› by blast
   }
  with ‹SIA ρ 𝒱 Tr⇘ES⇙› show ?thesis 
    unfolding BSIA_def using ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
    by auto 
qed 

lemma BSIA_implies_SIA_for_modified_view : 
  "⟦BSIA ρ' 𝒱' Tr⇘ES⇙; 𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N = {} , C = C⇘𝒱⇙ ⦈; ρ 𝒱 = ρ' 𝒱'⟧ ⟹ SIA ρ 𝒱 Tr⇘ES⇙" 
proof -
  assume "BSIA ρ' 𝒱' Tr⇘ES⇙"
     and "𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N = {} , C = C⇘𝒱⇙ ⦈" 
     and "ρ 𝒱 = ρ' 𝒱'"
  {
    fix α β c
    assume "c ∈ C⇘𝒱⇙"
       and "β  @ α ∈ Tr⇘ES⇙"
       and "α↿C⇘𝒱⇙ = []"
       and "Adm 𝒱 ρ Tr⇘ES⇙ β c"
    
    from ‹c ∈ C⇘𝒱⇙›  ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈›
    have "c ∈ C⇘𝒱'⇙"
      by auto     
    from ‹α↿C⇘𝒱⇙ = []› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› 
    have "α↿C⇘𝒱'⇙ = []"
      by auto
    from  ‹Adm 𝒱 ρ Tr⇘ES⇙ β c› ‹ρ 𝒱 = ρ' 𝒱'› 
    have "Adm 𝒱' ρ' Tr⇘ES⇙ β c"
      by (simp add: Adm_def)

    from ‹c ∈ C⇘𝒱'⇙› ‹β  @ α ∈ Tr⇘ES⇙› ‹α↿C⇘𝒱'⇙ = []› ‹Adm 𝒱' ρ' Tr⇘ES⇙ β c›
    obtain α' where "β @ [c] @ α' ∈ Tr⇘ES⇙"
                and " α' ↿ V⇘𝒱'⇙ = α ↿ V⇘𝒱'⇙"
                and " α' ↿ C⇘𝒱'⇙ = []"
      using ‹BSIA ρ' 𝒱' Tr⇘ES⇙›  unfolding BSIA_def by blast

    (*Show that α'=α*)    
    from ‹β  @ α ∈ Tr⇘ES⇙› validES
    have alpha_consists_of_events: "set α ⊆ E⇘ES⇙" 
      by (auto simp add: ES_valid_def traces_contain_events_def)

    from ‹β @ [c] @ α' ∈ Tr⇘ES⇙› validES
    have alpha'_consists_of_events: "set α' ⊆ E⇘ES⇙" 
      by (auto simp add: ES_valid_def traces_contain_events_def)  

    from ‹α' ↿ V⇘𝒱'⇙ = α ↿ V⇘𝒱'⇙› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N = {} , C = C⇘𝒱⇙ ⦈› 
    have "α'↿(V⇘𝒱⇙ ∪ N⇘𝒱⇙)=α↿(V⇘𝒱⇙ ∪ N⇘𝒱⇙)" by auto
    with ‹α' ↿ C⇘𝒱'⇙ = []›  ‹α↿C⇘𝒱⇙ = []› ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N = {} , C = C⇘𝒱⇙ ⦈›
    have "α'↿(V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙)=α↿(V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙)" 
      by (simp add: projection_on_union)
    with VIsViewOnE alpha_consists_of_events alpha'_consists_of_events
    have "α'=α" unfolding isViewOn_def 
      by (simp add: list_subset_iff_projection_neutral)

    hence  "β @ [c] @ α ∈ Tr⇘ES⇙ "
      using ‹β @ [c] @ α' ∈ Tr⇘ES⇙› by blast
   }
  with ‹BSIA ρ' 𝒱' Tr⇘ES⇙› show ?thesis 
    unfolding SIA_def using ‹𝒱' = ⦇ V = V⇘𝒱⇙ ∪ N⇘𝒱⇙ , N ={} , C = C⇘𝒱⇙ ⦈› by auto   
qed    
end

(* lemma taken from lemma 3.5.11 in Heiko Mantel's dissertation *)
lemma Adm_implies_Adm_for_modified_rho: 
"⟦ Adm 𝒱⇩2 ρ⇩2 Tr α e;ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1)⟧ ⟹ Adm 𝒱⇩1 ρ⇩1 Tr α e " 
proof -
  assume "Adm 𝒱⇩2 ρ⇩2 Tr α e"
    and  "ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1)"
  then obtain γ
    where "γ @ [e] ∈ Tr"
      and "γ ↿ ρ⇩2 𝒱⇩2 = α ↿ ρ⇩2 𝒱⇩2"
    unfolding Adm_def by auto
  thus "Adm 𝒱⇩1 ρ⇩1 Tr α e"
    unfolding Adm_def 
    using ‹ρ⇩1 𝒱⇩1 ⊆ ρ⇩2 𝒱⇩2› non_empty_projection_on_subset 
    by blast
qed

context BSPTaxonomyDifferentCorrections
begin

(* lemma taken from lemma 3.5.13 from Heiko Mantel's dissertation*)
lemma SI_implies_FCI: 
"(SI 𝒱 Tr⇘ES⇙) ⟹ FCI Γ 𝒱 Tr⇘ES⇙"
proof -    
   assume SI: "SI 𝒱 Tr⇘ES⇙"
    { 
    fix α β c v
    assume "c ∈ C⇘𝒱⇙  ∩ Υ⇘Γ⇙"
      and  "v ∈ V⇘𝒱⇙  ∩ ∇⇘Γ⇙"
      and  "β @ [v] @ α ∈ Tr⇘ES⇙"
      and alpha_C_empty: "α ↿ C⇘𝒱⇙ = []"
    moreover
    with VIsViewOnE  have "(v # α) ↿ C⇘𝒱⇙ = []" 
      unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto
    ultimately
    have "β @ [c , v] @ α ∈ Tr⇘ES⇙" using SI unfolding SI_def by auto
    with alpha_C_empty  
    have "∃α'. ∃δ'. 
              (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ [c] @ δ' @ [v] @ α') ∈  Tr⇘ES⇙ 
                ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = [])" 
      by (metis append.simps(1) append.simps(2) bot_least list.set(1))
  }    
  thus ?thesis 
    unfolding SI_def FCI_def by auto
qed

(* lemma taken from lemma 3.5.13 from Heiko Mantel's dissertation*)
lemma SIA_implies_FCIA: 
"(SIA ρ 𝒱 Tr⇘ES⇙) ⟹ FCIA ρ Γ 𝒱 Tr⇘ES⇙"
proof -    
   assume SIA: "SIA ρ 𝒱 Tr⇘ES⇙"
    { 
    fix α β c v
    assume "c ∈ C⇘𝒱⇙  ∩ Υ⇘Γ⇙"
      and  "v ∈ V⇘𝒱⇙  ∩ ∇⇘Γ⇙"
      and  "β @ [v] @ α ∈ Tr⇘ES⇙"
      and alpha_C_empty: "α ↿ C⇘𝒱⇙ = []"
      and "Adm 𝒱 ρ Tr⇘ES⇙ β c"
    moreover
    with VIsViewOnE  have "(v # α) ↿ C⇘𝒱⇙ = []" 
      unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto
    ultimately
    have "β @ [c , v] @ α ∈ Tr⇘ES⇙" using SIA unfolding SIA_def by auto
    with alpha_C_empty  
    have "∃α'. ∃δ'. 
              (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ [c] @ δ' @ [v] @ α') ∈  Tr⇘ES⇙  
                ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = [])" 
      by (metis append.simps(1) append.simps(2) bot_least list.set(1))
  }    
  thus ?thesis
    unfolding SIA_def FCIA_def by auto
qed

(* lemma taken from lemma 3.5.13 from Heiko Mantel's dissertation*)
lemma FCI_implies_FCIA: 
"(FCI Γ 𝒱 Tr⇘ES⇙) ⟹ FCIA ρ Γ 𝒱 Tr⇘ES⇙" 
proof-
  assume FCI: "FCI Γ 𝒱 Tr⇘ES⇙"
  {
    fix α β c v
    assume "c ∈ C⇘𝒱⇙  ∩ Υ⇘Γ⇙"
      and  "v ∈ V⇘𝒱⇙  ∩ ∇⇘Γ⇙"
      and  "β @ [v] @ α ∈ Tr⇘ES⇙"
      and  "α ↿ C⇘𝒱⇙ = []"
    with FCI have   "∃α' δ'. set δ' ⊆ N⇘𝒱⇙ ∩ Δ⇘Γ⇙ ∧
                         β @ [c] @ δ' @ [v] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []" 
                            unfolding FCI_def by auto   
  }
  thus ?thesis
    unfolding FCI_def FCIA_def by auto  
qed


(* Mantel's PhD thesis, Theorem 3.5.7 Trivially fulfilled BSPs*)
lemma Trivially_fulfilled_SR_C_empty:  
"C⇘𝒱⇙ = {} ⟹ SR 𝒱 Tr⇘ES⇙" 
proof -
  assume "C⇘𝒱⇙={}"
  {
    fix τ 
    assume "τ ∈ Tr⇘ES⇙"
    hence "τ=τ↿E⇘ES⇙" using  validES 
      unfolding  ES_valid_def traces_contain_events_def projection_def by auto
    with ‹C⇘𝒱⇙={}› have "τ=τ↿(V⇘𝒱⇙∪N⇘𝒱⇙)"
      using VIsViewOnE unfolding isViewOn_def by auto    
    with ‹τ ∈ Tr⇘ES⇙› have "τ↿(V⇘𝒱⇙∪N⇘𝒱⇙) ∈ Tr⇘ES⇙"
      by auto
  }
  thus ?thesis
    unfolding SR_def by auto
qed

lemma Trivially_fulfilled_R_C_empty: 
"C⇘𝒱⇙ = {} ⟹ R 𝒱 Tr⇘ES⇙" 
proof -
  assume "C⇘𝒱⇙={}"
  {
    fix τ 
    assume "τ ∈ Tr⇘ES⇙"
    hence "τ=τ↿E⇘ES⇙" using  validES 
      unfolding  ES_valid_def traces_contain_events_def projection_def by auto
    with ‹C⇘𝒱⇙={}› have "τ=τ↿(V⇘𝒱⇙∪N⇘𝒱⇙)"
      using VIsViewOnE unfolding isViewOn_def by auto    
    with ‹τ ∈ Tr⇘ES⇙› ‹C⇘𝒱⇙={}› have "∃τ' ∈ Tr⇘ES⇙. τ↿C⇘𝒱⇙=[] ∧ τ' ↿V⇘𝒱⇙=τ↿V⇘𝒱⇙" 
      unfolding projection_def by auto
  }
  thus ?thesis
    unfolding R_def by auto
qed

lemma Trivially_fulfilled_SD_C_empty:  
"C⇘𝒱⇙ = {} ⟹ SD 𝒱 Tr⇘ES⇙" 
  by (simp add: SD_def)

lemma Trivially_fulfilled_BSD_C_empty: 
"C⇘𝒱⇙ = {} ⟹ BSD 𝒱 Tr⇘ES⇙"
  by (simp add: BSD_def)

lemma Trivially_fulfilled_D_C_empty:  
"C⇘𝒱⇙ = {} ⟹ D 𝒱 Tr⇘ES⇙" 
  by (simp add: D_def)

lemma Trivially_fulfilled_FCD_C_empty:  
"C⇘𝒱⇙ = {} ⟹ FCD Γ 𝒱 Tr⇘ES⇙" 
  by (simp add: FCD_def)

lemma Trivially_fullfilled_R_V_empty: 
"V⇘𝒱⇙={} ⟹ R 𝒱 Tr⇘ES⇙"
proof - 
  assume "V⇘𝒱⇙={}"
  {
    fix τ
    assume "τ ∈ Tr⇘ES⇙"
    let ?τ'="[]"
    from ‹τ ∈ Tr⇘ES⇙›have "?τ' ∈ Tr⇘ES⇙" 
      using validES 
      unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
    with ‹V⇘𝒱⇙={}›
    have "∃τ' ∈ Tr⇘ES⇙. τ'↿C⇘𝒱⇙=[] ∧ τ'↿V⇘𝒱⇙=τ↿V⇘𝒱⇙"  
      by (metis projection_on_empty_trace projection_to_emptyset_is_empty_trace)
  }
  thus ?thesis
    unfolding R_def by auto  
qed

lemma Trivially_fulfilled_BSD_V_empty: 
"V⇘𝒱⇙ = {} ⟹ BSD 𝒱 Tr⇘ES⇙"
proof -
  assume "V⇘𝒱⇙={}"
  {
    fix α β c
    assume "β @ [c] @ α ∈ Tr⇘ES⇙"
      and "α↿C⇘𝒱⇙= []"  

    from ‹β @ [c] @ α ∈ Tr⇘ES⇙› have "β ∈ Tr⇘ES⇙"
      using validES 
      unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
 
    let ?α'="[]"
    from ‹β ∈ Tr⇘ES⇙› ‹V⇘𝒱⇙={}› 
    have "β@ ?α'∈Tr⇘ES⇙ ∧ ?α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ ?α'↿C⇘𝒱⇙ = []"
      by (simp add: projection_on_empty_trace projection_to_emptyset_is_empty_trace)
    hence
    "∃α'. 
      β @ α'∈Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []" by blast
  }
  thus ?thesis
    unfolding BSD_def by auto
qed

lemma Trivially_fulfilled_D_V_empty: 
"V⇘𝒱⇙ = {} ⟹ D 𝒱 Tr⇘ES⇙"
proof -
  assume "V⇘𝒱⇙={}"
  {
    fix α β c
    assume "β @ [c] @ α ∈ Tr⇘ES⇙"
      and "α↿C⇘𝒱⇙= []"  
    
    from ‹β @ [c] @ α ∈ Tr⇘ES⇙› have "β ∈ Tr⇘ES⇙"
      using validES 
      unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
    
    let ?β'=β and  ?α'="[]"
    from ‹β ∈ Tr⇘ES⇙› ‹V⇘𝒱⇙={}› 
    have "?β'@ ?α'∈Tr⇘ES⇙ ∧ ?α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ ?α'↿C⇘𝒱⇙ = [] ∧ ?β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙)"
      by (simp add: projection_on_empty_trace projection_to_emptyset_is_empty_trace)
    hence
    "∃α' β'. 
      β'@ α'∈Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = [] ∧ β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙)"
      by blast
  }
  thus ?thesis
    unfolding D_def by auto
qed

lemma Trivially_fulfilled_FCD_V_empty: 
"V⇘𝒱⇙ = {} ⟹ FCD Γ 𝒱 Tr⇘ES⇙"
  by (simp add: FCD_def)

(* Mantel's PhD thesis, Theorem 3.5.8 Trivially fulfilled BSPs*)
lemma Trivially_fulfilled_FCD_Nabla_Υ_empty: 
"⟦∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}⟧⟹ FCD Γ 𝒱 Tr⇘ES⇙" 
proof -
  assume "∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}"
  thus ?thesis
  proof(rule disjE)
    assume "∇⇘Γ⇙={}" thus ?thesis
      by (simp add: FCD_def)
  next
    assume " Υ⇘Γ⇙={}" thus ?thesis
      by (simp add: FCD_def)
  qed
qed

lemma Trivially_fulfilled_FCD_N_subseteq_Δ_and_BSD: 
"⟦N⇘𝒱⇙ ⊆ Δ⇘Γ⇙; BSD 𝒱 Tr⇘ES⇙⟧ ⟹ FCD Γ 𝒱 Tr⇘ES⇙"
proof -
  assume "N⇘𝒱⇙ ⊆ Δ⇘Γ⇙"
     and "BSD 𝒱 Tr⇘ES⇙"
  {
    fix α β c v
    assume "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
       and "v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
       and "β @ [c,v] @ α ∈ Tr⇘ES⇙"
       and "α↿C⇘𝒱⇙ = []"
    from ‹c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙› have "c ∈ C⇘𝒱⇙"
      by auto
    from ‹v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙› have "v ∈ V⇘𝒱⇙"
      by auto
    
    let ?α="[v] @ α"
    from ‹v ∈ V⇘𝒱⇙› ‹α↿C⇘𝒱⇙ = []› have "?α↿C⇘𝒱⇙=[]"
      using VIsViewOnE 
      unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto
    from ‹β @ [c,v] @ α ∈ Tr⇘ES⇙› have "β @ [c] @ ?α ∈ Tr⇘ES⇙"
      by auto
    
    from ‹BSD 𝒱 Tr⇘ES⇙› 
    obtain α' 
      where "β @ α' ∈ Tr⇘ES⇙"
        and "α'↿V⇘𝒱⇙ = ([v] @ α)↿V⇘𝒱⇙"
        and "α'↿C⇘𝒱⇙ = []"
      using ‹c ∈ C⇘𝒱⇙›  ‹β @ [c] @ ?α ∈ Tr⇘ES⇙› ‹?α↿C⇘𝒱⇙ = []› 
      unfolding BSD_def by auto 

    from‹v ∈ V⇘𝒱⇙› ‹α'↿V⇘𝒱⇙ = ([v] @ α)↿V⇘𝒱⇙› have "α'↿V⇘𝒱⇙ = [v] @ α↿V⇘𝒱⇙" 
      by (simp add: projection_def)
    then obtain δ α''
      where "α'=δ @ [v] @ α''"
        and "δ↿V⇘𝒱⇙ = []"
        and "α''↿V⇘𝒱⇙ = α↿V⇘𝒱⇙"
       using projection_split_first_with_suffix by fastforce 

    from ‹α'↿C⇘𝒱⇙ = []› ‹α'=δ @ [v] @ α''› have "δ↿C⇘𝒱⇙=[]"
      by (metis append_is_Nil_conv projection_concatenation_commute) 
    from ‹α'↿C⇘𝒱⇙ = []› ‹α'=δ @ [v] @ α''› have "α''↿C⇘𝒱⇙=[]" 
      by (metis append_is_Nil_conv projection_concatenation_commute) 
    
    from ‹β @ α' ∈ Tr⇘ES⇙› have "set α' ⊆ E⇘ES⇙" using validES 
      unfolding ES_valid_def traces_contain_events_def by auto
    with  ‹α'=δ @ [v] @ α''› have "set δ ⊆ E⇘ES⇙"
      by auto
    with  ‹δ↿C⇘𝒱⇙=[]› ‹δ↿V⇘𝒱⇙ = []› ‹N⇘𝒱⇙ ⊆ Δ⇘Γ⇙›
    have "(set δ) ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)" 
      using VIsViewOnE projection_empty_implies_absence_of_events  
      unfolding isViewOn_def projection_def by blast
    
    let ?β=β and ?δ'=δ and ?α'=α''
    from ‹(set δ) ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)› ‹β @ α' ∈ Tr⇘ES⇙› ‹α'=δ @ [v] @ α''› 
            ‹α''↿V⇘𝒱⇙ = α↿V⇘𝒱⇙› ‹α''↿C⇘𝒱⇙=[]›
    have "(set ?δ')⊆(N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ?β @ ?δ' @ [v] @ ?α' ∈ Tr⇘ES⇙ ∧ ?α'↿V⇘𝒱⇙=α↿V⇘𝒱⇙ ∧ ?α'↿C⇘𝒱⇙=[]"
      by auto
    hence "∃α''' δ''. (set δ'') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ (β @ δ'' @ [v] @ α''') ∈ Tr⇘ES⇙ 
              ∧ α''' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α''' ↿ C⇘𝒱⇙ = []" 
      by auto 
  }
  thus ?thesis
    unfolding FCD_def by auto  
qed

(* Mantel's PhD thesis, Theorem 3.5.16 Trivially fulfilled BSPs*)
lemma Trivially_fulfilled_SI_C_empty:  
"C⇘𝒱⇙ = {} ⟹ SI 𝒱 Tr⇘ES⇙" 
  by (simp add: SI_def)

lemma Trivially_fulfilled_BSI_C_empty: 
"C⇘𝒱⇙ = {} ⟹ BSI 𝒱 Tr⇘ES⇙"
  by (simp add: BSI_def)

lemma Trivially_fulfilled_I_C_empty:  
"C⇘𝒱⇙ = {} ⟹ I 𝒱 Tr⇘ES⇙" 
  by (simp add: I_def)

lemma Trivially_fulfilled_FCI_C_empty:  
"C⇘𝒱⇙ = {} ⟹ FCI Γ 𝒱 Tr⇘ES⇙"
  by (simp add: FCI_def)

lemma Trivially_fulfilled_SIA_C_empty:  
"C⇘𝒱⇙ = {} ⟹ SIA ρ 𝒱 Tr⇘ES⇙" 
  by (simp add: SIA_def)

lemma Trivially_fulfilled_BSIA_C_empty: 
"C⇘𝒱⇙ = {} ⟹ BSIA ρ 𝒱 Tr⇘ES⇙"
  by (simp add: BSIA_def)

lemma Trivially_fulfilled_IA_C_empty:  
"C⇘𝒱⇙ = {} ⟹ IA ρ 𝒱 Tr⇘ES⇙" 
  by (simp add: IA_def)

lemma Trivially_fulfilled_FCIA_C_empty:  
"C⇘𝒱⇙ = {} ⟹ FCIA Γ ρ 𝒱 Tr⇘ES⇙" 
  by (simp add: FCIA_def)

lemma Trivially_fulfilled_FCI_V_empty: 
"V⇘𝒱⇙ = {} ⟹ FCI Γ 𝒱 Tr⇘ES⇙"
  by (simp add: FCI_def)

lemma Trivially_fulfilled_FCIA_V_empty: 
"V⇘𝒱⇙ = {} ⟹ FCIA ρ Γ 𝒱 Tr⇘ES⇙"
  by (simp add: FCIA_def)

lemma Trivially_fulfilled_BSIA_V_empty_rho_subseteq_C_N: 
"⟦V⇘𝒱⇙ = {}; ρ 𝒱 ⊇ (C⇘𝒱⇙ ∪ N⇘𝒱⇙) ⟧ ⟹ BSIA ρ  𝒱 Tr⇘ES⇙" 
proof -
  assume "V⇘𝒱⇙={}"
     and "ρ 𝒱 ⊇ (C⇘𝒱⇙ ∪ N⇘𝒱⇙)"
  {
    fix α β c 
    assume "c ∈ C⇘𝒱⇙" 
       and "β @ α ∈ Tr⇘ES⇙"
       and "α↿C⇘𝒱⇙=[]"
       and "Adm 𝒱 ρ Tr⇘ES⇙ β c"
    from ‹Adm 𝒱 ρ Tr⇘ES⇙ β c› 
    obtain γ 
      where "γ @ [c] ∈ Tr⇘ES⇙"
        and "γ↿(ρ 𝒱) = β↿(ρ 𝒱)"
      unfolding Adm_def by auto
    from this(1) have "γ ∈ Tr⇘ES⇙" 
      using validES 
      unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto 
    moreover
    from ‹β @ α ∈ Tr⇘ES⇙› have "β ∈ Tr⇘ES⇙"
      using validES
      unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
    ultimately
    have "β↿E⇘ES⇙=γ↿E⇘ES⇙" 
      using validES VIsViewOnE ‹V⇘𝒱⇙={}› ‹γ↿(ρ 𝒱) = β↿(ρ 𝒱)› ‹ρ 𝒱 ⊇ (C⇘𝒱⇙ ∪ N⇘𝒱⇙)› 
        non_empty_projection_on_subset
      unfolding ES_valid_def isViewOn_def traces_contain_events_def 
      by (metis  empty_subsetI sup_absorb2 sup_commute)
    hence "β @ [c] ∈ Tr⇘ES⇙" using validES ‹γ @ [c] ∈ Tr⇘ES⇙› ‹β ∈ Tr⇘ES⇙› ‹γ ∈ Tr⇘ES⇙›
      unfolding ES_valid_def traces_contain_events_def 
      by (metis  list_subset_iff_projection_neutral subsetI)
    
    let ?α'="[]"
    from ‹β @ [c] ∈ Tr⇘ES⇙› ‹V⇘𝒱⇙ = {}› 
    have "β @ [c] @ ?α' ∈Tr⇘ES⇙ ∧ ?α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ ?α'↿C⇘𝒱⇙ = []" 
      by (simp add: projection_on_empty_trace projection_to_emptyset_is_empty_trace)
    hence "∃ α'. β @ [c] @ α' ∈Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []" 
      by auto  
  }
  thus ?thesis
    unfolding BSIA_def by auto
qed

lemma Trivially_fulfilled_IA_V_empty_rho_subseteq_C_N: 
"⟦V⇘𝒱⇙ = {}; ρ 𝒱 ⊇ (C⇘𝒱⇙ ∪ N⇘𝒱⇙) ⟧ ⟹ IA ρ  𝒱 Tr⇘ES⇙" 
proof -
  assume "V⇘𝒱⇙={}"
     and "ρ 𝒱 ⊇ (C⇘𝒱⇙ ∪ N⇘𝒱⇙)"
  {
    fix α β c 
    assume "c ∈ C⇘𝒱⇙" 
       and "β @ α ∈ Tr⇘ES⇙"
       and "α↿C⇘𝒱⇙=[]"
       and "Adm 𝒱 ρ Tr⇘ES⇙ β c"
    from ‹Adm 𝒱 ρ Tr⇘ES⇙ β c›
    obtain γ 
      where "γ @ [c] ∈ Tr⇘ES⇙"
        and "γ↿(ρ 𝒱) = β↿(ρ 𝒱)"
        unfolding Adm_def by auto
    from this(1) have "γ ∈ Tr⇘ES⇙"
      using validES 
      unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto 
    moreover
    from ‹β @ α ∈ Tr⇘ES⇙› have "β ∈ Tr⇘ES⇙" using validES
      unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
    ultimately
    have "β↿E⇘ES⇙=γ↿E⇘ES⇙" 
      using validES VIsViewOnE ‹V⇘𝒱⇙={}› ‹γ↿(ρ 𝒱) = β↿(ρ 𝒱)› ‹ρ 𝒱 ⊇ (C⇘𝒱⇙ ∪ N⇘𝒱⇙)› 
        non_empty_projection_on_subset
      unfolding ES_valid_def isViewOn_def traces_contain_events_def 
      by (metis  empty_subsetI sup_absorb2 sup_commute)
    hence "β @ [c] ∈ Tr⇘ES⇙" using validES ‹γ @ [c] ∈ Tr⇘ES⇙› ‹β ∈ Tr⇘ES⇙› ‹γ ∈ Tr⇘ES⇙›
      unfolding ES_valid_def traces_contain_events_def 
      by (metis  list_subset_iff_projection_neutral subsetI)
    
    let ?β'=β and ?α'="[]"
    from ‹β @ [c] ∈ Tr⇘ES⇙› ‹V⇘𝒱⇙ = {}› 
    have "?β' @ [c] @ ?α' ∈Tr⇘ES⇙ ∧ ?α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ ?α'↿C⇘𝒱⇙ = [] 
              ∧ ?β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙)" 
      by (simp add: projection_on_empty_trace projection_to_emptyset_is_empty_trace)
    hence "∃ α' β'. 
              β' @ [c] @ α' ∈Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = [] 
                ∧ β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙)"
      by auto  
  }
  thus ?thesis
    unfolding IA_def by auto
qed

lemma Trivially_fulfilled_BSI_V_empty_total_ES_C: 
"⟦V⇘𝒱⇙ = {}; total ES C⇘𝒱⇙ ⟧ ⟹ BSI 𝒱 Tr⇘ES⇙" 
proof -
  assume "V⇘𝒱⇙ = {}"
     and "total ES C⇘𝒱⇙"  
  {
   fix α β c
   assume "β @ α ∈ Tr⇘ES⇙"
      and "α↿C⇘𝒱⇙=[]"
      and "c ∈ C⇘𝒱⇙"
   from ‹β @ α ∈ Tr⇘ES⇙› have "β ∈ Tr⇘ES⇙" 
    using validES
    unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
   with ‹total ES C⇘𝒱⇙› have "β @ [c] ∈ Tr⇘ES⇙" 
    using ‹c ∈ C⇘𝒱⇙›  unfolding total_def by auto
   moreover
   from ‹V⇘𝒱⇙ = {}› have "α↿V⇘𝒱⇙=[]"
     unfolding projection_def by auto
   ultimately 
   have "∃α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇙=α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙=[]" 
    using ‹α ↿ C⇘𝒱⇙ = []›  by (metis append_Nil2 projection_idempotent)     
  }
  thus ?thesis
    unfolding BSI_def by auto
qed

lemma Trivially_fulfilled_I_V_empty_total_ES_C: 
"⟦V⇘𝒱⇙ = {}; total ES C⇘𝒱⇙ ⟧ ⟹ I 𝒱 Tr⇘ES⇙" 
proof -
  assume "V⇘𝒱⇙ = {}"
     and "total ES C⇘𝒱⇙"  
  {
   fix α β c
   assume "c ∈ C⇘𝒱⇙"
      and "β @ α ∈ Tr⇘ES⇙"
      and "α↿C⇘𝒱⇙=[]"
   from ‹β @ α ∈ Tr⇘ES⇙› have "β ∈ Tr⇘ES⇙" 
     using validES
     unfolding ES_valid_def traces_prefixclosed_def prefixclosed_def prefix_def by auto
   with ‹total ES C⇘𝒱⇙› have "β @ [c] ∈ Tr⇘ES⇙"
     using ‹c ∈ C⇘𝒱⇙›  unfolding total_def by auto
   moreover
   from ‹V⇘𝒱⇙ = {}› have "α↿V⇘𝒱⇙=[]"
     unfolding projection_def by auto
   ultimately 
   have "∃β' α'. 
          β' @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇙=α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙=[] ∧ β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙)" 
    using ‹α ↿ C⇘𝒱⇙ = []› by (metis append_Nil2 projection_idempotent)     
  }
  thus ?thesis
    unfolding I_def by blast
qed

(* Mantel's PhD thesis, Theorem 3.5.17 Trivially fulfilled BSPs*)
lemma Trivially_fulfilled_FCI_Nabla_Υ_empty: 
"⟦∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}⟧⟹ FCI Γ 𝒱 Tr⇘ES⇙" 
proof -
  assume "∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}"
  thus ?thesis
  proof(rule disjE)
    assume "∇⇘Γ⇙={}" thus ?thesis
      by (simp add: FCI_def)
  next
    assume " Υ⇘Γ⇙={}" thus ?thesis
      by (simp add: FCI_def)
  qed
qed

lemma Trivially_fulfilled_FCIA_Nabla_Υ_empty: 
"⟦∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}⟧⟹ FCIA ρ Γ 𝒱 Tr⇘ES⇙" 
proof -
  assume "∇⇘Γ⇙={} ∨ Υ⇘Γ⇙={}"
  thus ?thesis
  proof(rule disjE)
    assume "∇⇘Γ⇙={}" thus ?thesis
      by (simp add: FCIA_def)
  next
    assume " Υ⇘Γ⇙={}" thus ?thesis
      by (simp add: FCIA_def)
  qed
qed

lemma Trivially_fulfilled_FCI_N_subseteq_Δ_and_BSI: 
"⟦N⇘𝒱⇙ ⊆ Δ⇘Γ⇙; BSI 𝒱 Tr⇘ES⇙⟧ ⟹ FCI Γ 𝒱 Tr⇘ES⇙" 
proof -
  assume "N⇘𝒱⇙ ⊆ Δ⇘Γ⇙"
     and "BSI 𝒱 Tr⇘ES⇙"
  {
    fix α β c v
    assume "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
       and "v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
       and "β @ [v] @ α ∈ Tr⇘ES⇙"
       and "α↿C⇘𝒱⇙ = []"
    from ‹c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙› have "c ∈ C⇘𝒱⇙"
      by auto
    from ‹v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙› have "v ∈ V⇘𝒱⇙"
      by auto
    
    let ?α="[v] @ α"
    from ‹v ∈ V⇘𝒱⇙› ‹α↿C⇘𝒱⇙ = []› have "?α↿C⇘𝒱⇙=[]"
      using VIsViewOnE 
      unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto
    from ‹β @ [v] @ α ∈ Tr⇘ES⇙› have "β @  ?α ∈ Tr⇘ES⇙"
      by auto
    
    from ‹BSI 𝒱 Tr⇘ES⇙› 
    obtain α' 
      where "β @ [c] @ α' ∈ Tr⇘ES⇙"
        and "α'↿V⇘𝒱⇙ = ([v] @ α)↿V⇘𝒱⇙"
        and "α'↿C⇘𝒱⇙ = []"
      using ‹c ∈ C⇘𝒱⇙›  ‹β @ ?α ∈ Tr⇘ES⇙› ‹?α↿C⇘𝒱⇙ = []› 
      unfolding BSI_def by blast 

    from‹v ∈ V⇘𝒱⇙› ‹α'↿V⇘𝒱⇙ = ([v] @ α)↿V⇘𝒱⇙› have "α'↿V⇘𝒱⇙ = [v] @ α↿V⇘𝒱⇙" 
      by (simp add: projection_def)
    then 
    obtain δ α''
      where "α'=δ @ [v] @ α''"
        and "δ↿V⇘𝒱⇙ = []"
        and "α''↿V⇘𝒱⇙ = α↿V⇘𝒱⇙"
       using projection_split_first_with_suffix by fastforce 

    from ‹α'↿C⇘𝒱⇙ = []› ‹α'=δ @ [v] @ α''› have "δ↿C⇘𝒱⇙=[]"
      by (metis append_is_Nil_conv projection_concatenation_commute) 
    from ‹α'↿C⇘𝒱⇙ = []› ‹α'=δ @ [v] @ α''› have "α''↿C⇘𝒱⇙=[]" 
      by (metis append_is_Nil_conv projection_concatenation_commute) 
    
    from ‹β @ [c] @ α' ∈ Tr⇘ES⇙› have "set α' ⊆ E⇘ES⇙" 
      using validES 
      unfolding ES_valid_def traces_contain_events_def by auto
    with  ‹α'=δ @ [v] @ α''› have "set δ ⊆ E⇘ES⇙" 
      by auto
    with  ‹δ↿C⇘𝒱⇙=[]› ‹δ↿V⇘𝒱⇙ = []› ‹N⇘𝒱⇙ ⊆ Δ⇘Γ⇙›
    have "(set δ) ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)"
      using VIsViewOnE projection_empty_implies_absence_of_events  
      unfolding isViewOn_def projection_def by blast
    
    let ?β=β and ?δ'=δ and ?α'=α''
    from ‹(set δ) ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)› ‹β @ [c] @ α' ∈ Tr⇘ES⇙› ‹α'=δ @ [v] @ α''› 
            ‹α''↿V⇘𝒱⇙ = α↿V⇘𝒱⇙› ‹α''↿C⇘𝒱⇙=[]›
    have "(set ?δ')⊆(N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ?β @ [c] @ ?δ' @ [v] @ ?α' ∈ Tr⇘ES⇙ ∧ ?α'↿V⇘𝒱⇙=α↿V⇘𝒱⇙ ∧ ?α'↿C⇘𝒱⇙=[]"
      by auto
    hence "∃α''' δ''. (set δ'') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ (β @ [c] @ δ'' @ [v] @ α''') ∈ Tr⇘ES⇙ 
              ∧ α''' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α''' ↿ C⇘𝒱⇙ = []" 
      by auto 
  }
  thus ?thesis
    unfolding FCI_def by auto  
qed

lemma Trivially_fulfilled_FCIA_N_subseteq_Δ_and_BSIA: 
"⟦N⇘𝒱⇙ ⊆ Δ⇘Γ⇙; BSIA ρ 𝒱 Tr⇘ES⇙⟧ ⟹ FCIA ρ Γ 𝒱 Tr⇘ES⇙" 
proof -
  assume "N⇘𝒱⇙ ⊆ Δ⇘Γ⇙"
     and "BSIA ρ 𝒱 Tr⇘ES⇙"
  {
    fix α β c v
    assume "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
       and "v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
       and "β @ [v] @ α ∈ Tr⇘ES⇙"
       and "α↿C⇘𝒱⇙ = []"
       and "Adm 𝒱 ρ Tr⇘ES⇙ β c"
    from ‹c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙› have "c ∈ C⇘𝒱⇙" 
      by auto
    from ‹v ∈ V⇘𝒱⇙ ∩ ∇⇘Γ⇙› have "v ∈ V⇘𝒱⇙" 
      by auto
    
    let ?α="[v] @ α"
    from ‹v ∈ V⇘𝒱⇙› ‹α↿C⇘𝒱⇙ = []› have "?α↿C⇘𝒱⇙=[]"
      using VIsViewOnE 
      unfolding isViewOn_def V_valid_def VC_disjoint_def projection_def by auto
    from ‹β @ [v] @ α ∈ Tr⇘ES⇙› have "β @  ?α ∈ Tr⇘ES⇙" 
      by auto
    
    from ‹BSIA ρ 𝒱 Tr⇘ES⇙› 
    obtain α' 
      where "β @ [c] @ α' ∈ Tr⇘ES⇙"
        and "α'↿V⇘𝒱⇙ = ([v] @ α)↿V⇘𝒱⇙"
        and "α'↿C⇘𝒱⇙ = []"
      using ‹c ∈ C⇘𝒱⇙›  ‹β @ ?α ∈ Tr⇘ES⇙› ‹?α↿C⇘𝒱⇙ = []› ‹Adm 𝒱 ρ Tr⇘ES⇙ β c› 
      unfolding BSIA_def by blast 

    from‹v ∈ V⇘𝒱⇙› ‹α'↿V⇘𝒱⇙ = ([v] @ α)↿V⇘𝒱⇙› have "α'↿V⇘𝒱⇙ = [v] @ α↿V⇘𝒱⇙" 
      by (simp add: projection_def)
    then 
    obtain δ α''
      where "α'=δ @ [v] @ α''"
        and "δ↿V⇘𝒱⇙ = []"
        and "α''↿V⇘𝒱⇙ = α↿V⇘𝒱⇙"
       using projection_split_first_with_suffix by fastforce 

    from ‹α'↿C⇘𝒱⇙ = []› ‹α'=δ @ [v] @ α''› have "δ↿C⇘𝒱⇙=[]"
      by (metis append_is_Nil_conv projection_concatenation_commute) 
    from ‹α'↿C⇘𝒱⇙ = []› ‹α'=δ @ [v] @ α''› have "α''↿C⇘𝒱⇙=[]" 
      by (metis append_is_Nil_conv projection_concatenation_commute) 
    
    from ‹β @ [c] @ α' ∈ Tr⇘ES⇙› have "set α' ⊆ E⇘ES⇙" 
      using validES 
      unfolding ES_valid_def traces_contain_events_def by auto
    with  ‹α'=δ @ [v] @ α''› have "set δ ⊆ E⇘ES⇙" 
      by auto
    with  ‹δ↿C⇘𝒱⇙=[]› ‹δ↿V⇘𝒱⇙ = []› ‹N⇘𝒱⇙ ⊆ Δ⇘Γ⇙›
    have "(set δ) ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)" using VIsViewOnE projection_empty_implies_absence_of_events  
      unfolding isViewOn_def projection_def by blast
    
    let ?β=β and ?δ'=δ and ?α'=α''
    from ‹(set δ) ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)› ‹β @ [c] @ α' ∈ Tr⇘ES⇙› ‹α'=δ @ [v] @ α''› 
            ‹α''↿V⇘𝒱⇙ = α↿V⇘𝒱⇙› ‹α''↿C⇘𝒱⇙=[]›
    have "(set ?δ')⊆(N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ?β @ [c] @ ?δ' @ [v] @ ?α' ∈ Tr⇘ES⇙ ∧ ?α'↿V⇘𝒱⇙=α↿V⇘𝒱⇙ ∧ ?α'↿C⇘𝒱⇙=[]"
      by auto
    hence "∃α''' δ''. (set δ'') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ (β @ [c] @ δ'' @ [v] @ α''') ∈ Tr⇘ES⇙ 
              ∧ α''' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α''' ↿ C⇘𝒱⇙ = []" 
      by auto 
  }
  thus ?thesis
    unfolding FCIA_def by auto  
qed

end

context BSPTaxonomyDifferentViewsFirstDim
begin
(* lemma taken from lemma 3.5.2 in Heiko Mantel's dissertation *)
lemma R_implies_R_for_modified_view: 
"R 𝒱⇩1 Tr⇘ES⇙ ⟹ R 𝒱⇩2 Tr⇘ES⇙"
proof -
  assume R_𝒱⇩1: "R 𝒱⇩1 Tr⇘ES⇙"
  {
    fix τ
    assume "τ ∈ Tr⇘ES⇙" 
    with R_𝒱⇩1 have "∃ τ' ∈ Tr⇘ES⇙.  τ' ↿ C⇘𝒱⇩1⇙ = [] ∧ τ' ↿ V⇘𝒱⇩1⇙ = τ ↿ V⇘𝒱⇩1⇙"
      unfolding R_def by auto 
    hence "∃ τ' ∈ Tr⇘ES⇙.  τ' ↿ C⇘𝒱⇩2⇙ = [] ∧ τ' ↿ V⇘𝒱⇩2⇙ = τ ↿ V⇘𝒱⇩2⇙" 
      using  V2_subset_V1  C2_subset_C1  non_empty_projection_on_subset projection_on_subset by blast
  }
  thus ?thesis
    unfolding R_def by auto
qed

lemma BSD_implies_BSD_for_modified_view: 
"BSD 𝒱⇩1 Tr⇘ES⇙⟹ BSD 𝒱⇩2 Tr⇘ES⇙"
proof- 
  assume BSD_𝒱⇩1: "BSD 𝒱⇩1 Tr⇘ES⇙"
  { 
    fix α β c n 
    assume  c_in_C⇩2: "c ∈ C⇘𝒱⇩2⇙" 
    from C2_subset_C1  c_in_C⇩2  have c_in_C⇩1: "c ∈ C⇘𝒱⇩1⇙"
      by auto 
    have "⟦β @ [c] @ α ∈ Tr⇘ES⇙; α ↿ C⇘𝒱⇩2⇙=[]; n= length(α ↿ C⇘𝒱⇩1⇙)⟧
            ⟹ ∃ α'. β @ α' ∈ Tr⇘ES⇙ ∧ α'↿ V⇘𝒱⇩2⇙ = α ↿V⇘𝒱⇩2⇙  ∧ α' ↿C⇘𝒱⇩2⇙ = []"
    proof(induct n arbitrary: α  )        
      case 0
        from "0.prems"(3) have "α ↿ C⇘𝒱⇩1⇙ = []" by auto
        with c_in_C⇩1 "0.prems"(1) 
          have "∃ α'. β @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙ ∧ α' ↿C⇘𝒱⇩1⇙ =[]"
          using BSD_𝒱⇩1 unfolding BSD_def by auto
        then 
        obtain α' where "β @ α' ∈ Tr⇘ES⇙"
                    and "α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙"
                    and "α' ↿C⇘𝒱⇩1⇙ =[]"
          by auto
        from V2_subset_V1  ‹α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙›  have  "α'↿ V⇘𝒱⇩2⇙ = α ↿V⇘𝒱⇩2⇙" 
          using non_empty_projection_on_subset by blast
        moreover
        from ‹α' ↿C⇘𝒱⇩1⇙ =[]›  C2_subset_C1 have "α' ↿ C⇘𝒱⇩2⇙ = []" 
          using projection_on_subset by auto
        ultimately
        show ?case 
          using ‹β @ α' ∈ Tr⇘ES⇙› by auto
      next
      case (Suc n)
        from "Suc.prems"(3) projection_split_last[OF "Suc.prems"(3)]  
        obtain γ⇩1 γ⇩2 c⇩1 where c⇩1_in_C⇩1: "c⇩1 ∈ C⇘𝒱⇩1⇙"
                         and "α = γ⇩1 @ [c⇩1] @ γ⇩2" 
                         and "γ⇩2 ↿C⇘𝒱⇩1⇙ = []" 
                         and "n = length((γ⇩1 @ γ⇩2)↿ C⇘𝒱⇩1⇙)"
          by auto
        from  "Suc.prems"(2) ‹α = γ⇩1 @ [c⇩1] @ γ⇩2› have "γ⇩1 ↿ C⇘𝒱⇩2⇙ = []"
          by (simp add: projection_concatenation_commute)
        from  "Suc.prems"(1) ‹α = γ⇩1 @ [c⇩1] @ γ⇩2› 
        obtain β' where "β'=β @ [c] @ γ⇩1"
                    and "β' @ [c⇩1] @ γ⇩2 ∈ Tr⇘ES⇙"
          by auto
        from ‹β' @ [c⇩1] @ γ⇩2 ∈ Tr⇘ES⇙›  ‹γ⇩2 ↿C⇘𝒱⇩1⇙ = []› ‹c⇩1 ∈ C⇘𝒱⇩1⇙› 
        obtain γ⇩2' where " β' @ γ⇩2' ∈ Tr⇘ES⇙"
                    and "γ⇩2' ↿ V⇘𝒱⇩1⇙ = γ⇩2 ↿ V⇘𝒱⇩1⇙"
                    and "γ⇩2' ↿C⇘𝒱⇩1⇙ =[]"
          using BSD_𝒱⇩1  unfolding BSD_def by auto
        from ‹β'=β @ [c] @ γ⇩1› ‹β' @ γ⇩2' ∈ Tr⇘ES⇙›  have "β @ [c] @ γ⇩1 @ γ⇩2' ∈ Tr⇘ES⇙"
          by auto 
        moreover
        from  ‹γ⇩1 ↿ C⇘𝒱⇩2⇙=[]›  ‹γ⇩2' ↿C⇘𝒱⇩1⇙ =[]› C2_subset_C1 have "(γ⇩1 @ γ⇩2') ↿ C⇘𝒱⇩2⇙ =[]" 
          by (metis append_Nil projection_concatenation_commute projection_on_subset)
        moreover
        from ‹n = length((γ⇩1 @ γ⇩2)↿ C⇘𝒱⇩1⇙)› ‹γ⇩2 ↿C⇘𝒱⇩1⇙ = []› ‹γ⇩2' ↿C⇘𝒱⇩1⇙ =[]› 
        have "n = length((γ⇩1 @ γ⇩2')↿ C⇘𝒱⇩1⇙)"
          by (simp add: projection_concatenation_commute)
        ultimately 
        have witness: "∃ α'. β @ α' ∈ Tr⇘ES⇙ ∧ α'↿ V⇘𝒱⇩2⇙ = (γ⇩1 @ γ⇩2') ↿V⇘𝒱⇩2⇙  ∧ α' ↿C⇘𝒱⇩2⇙ = []" 
          using  Suc.hyps by auto
        
        from  𝒱⇩1IsViewOnE 𝒱⇩2IsViewOnE V2_subset_V1 C2_subset_C1  c⇩1_in_C⇩1 have "c⇩1 ∉ V⇘𝒱⇩2⇙"  
          unfolding isViewOn_def V_valid_def  VC_disjoint_def by auto
        with ‹α = γ⇩1 @ [c⇩1] @ γ⇩2› have "α ↿ V⇘𝒱⇩2⇙ = (γ⇩1 @ γ⇩2) ↿ V⇘𝒱⇩2⇙" 
          unfolding projection_def by auto
        hence "α ↿ V⇘𝒱⇩2⇙ = γ⇩1 ↿ V⇘𝒱⇩2⇙ @ γ⇩2 ↿ V⇘𝒱⇩2⇙ " 
          using projection_concatenation_commute by auto
        with V2_subset_V1 ‹γ⇩2' ↿ V⇘𝒱⇩1⇙ = γ⇩2 ↿ V⇘𝒱⇩1⇙›
        have "γ⇩1 ↿ V⇘𝒱⇩2⇙ @ γ⇩2 ↿ V⇘𝒱⇩2⇙ = γ⇩1↿ V⇘𝒱⇩2⇙ @ γ⇩2' ↿ V⇘𝒱⇩2⇙" 
          using non_empty_projection_on_subset by metis
        with ‹α ↿ V⇘𝒱⇩2⇙ = γ⇩1 ↿ V⇘𝒱⇩2⇙ @ γ⇩2 ↿ V⇘𝒱⇩2⇙› have "α ↿ V⇘𝒱⇩2⇙ = (γ⇩1 @ γ⇩2') ↿ V⇘𝒱⇩2⇙"
          by (simp add: projection_concatenation_commute)
       
       from witness  ‹α ↿ V⇘𝒱⇩2⇙ = (γ⇩1 @ γ⇩2') ↿ V⇘𝒱⇩2⇙› 
       show ?case 
         by auto
     qed          
 }  
  thus ?thesis 
    unfolding BSD_def by auto
qed

lemma D_implies_D_for_modified_view: 
"D 𝒱⇩1 Tr⇘ES⇙ ⟹ D 𝒱⇩2 Tr⇘ES⇙"
proof- 
  assume D_𝒱⇩1: "D 𝒱⇩1 Tr⇘ES⇙"
   from V2_subset_V1 C2_subset_C1
    have V⇩2_union_C⇩2_subset_V⇩1_union_C⇩1: "V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙ ⊆ V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙" by auto
  { 
    fix α β c n 
    assume  c_in_C⇩2: "c ∈ C⇘𝒱⇩2⇙" 
    from C2_subset_C1  c_in_C⇩2  have c_in_C⇩1: "c ∈ C⇘𝒱⇩1⇙" 
      by auto 
    have "⟦β @ [c] @ α ∈ Tr⇘ES⇙; α ↿ C⇘𝒱⇩2⇙=[]; n= length(α ↿ C⇘𝒱⇩1⇙)⟧
            ⟹ ∃ α' β'. 
                  β' @ α' ∈ Tr⇘ES⇙  ∧ α'↿ V⇘𝒱⇩2⇙ = α ↿V⇘𝒱⇩2⇙  ∧ α' ↿C⇘𝒱⇩2⇙ = [] 
                     ∧ β' ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) = β ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) "
    proof(induct n arbitrary: α β )        
      case 0
        from "0.prems"(3) have "α ↿ C⇘𝒱⇩1⇙ = []" by auto
        with c_in_C⇩1 "0.prems"(1) 
        have "∃ α' β'. 
                β' @ α' ∈ Tr⇘ES⇙  ∧ α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙ ∧ α' ↿C⇘𝒱⇩1⇙ =[] 
                  ∧ β' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)"
          using D_𝒱⇩1 unfolding D_def by fastforce
        then 
        obtain β' α' where "β' @ α' ∈ Tr⇘ES⇙"
                      and "α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙"
                      and "α' ↿C⇘𝒱⇩1⇙ =[]"
                      and "β' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)" 
          by auto
        from V2_subset_V1  ‹α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙›  have  "α'↿ V⇘𝒱⇩2⇙ = α ↿V⇘𝒱⇩2⇙" 
          using non_empty_projection_on_subset by blast
        moreover
        from ‹α' ↿C⇘𝒱⇩1⇙ =[]›  C2_subset_C1 have "α' ↿ C⇘𝒱⇩2⇙ = []"
          using projection_on_subset by auto
        moreover
        from ‹β' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)›  V⇩2_union_C⇩2_subset_V⇩1_union_C⇩1 
        have "β' ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) = β ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙)"
          using non_empty_projection_on_subset by blast
        ultimately
        show ?case 
          using ‹β' @ α' ∈ Tr⇘ES⇙› by auto
      next
      case (Suc n)
        from "Suc.prems"(3) projection_split_last[OF "Suc.prems"(3)]  
        obtain γ⇩1 γ⇩2 c⇩1 where c⇩1_in_C⇩1: "c⇩1 ∈ C⇘𝒱⇩1⇙"
                         and "α = γ⇩1 @ [c⇩1] @ γ⇩2" 
                         and "γ⇩2 ↿C⇘𝒱⇩1⇙ = []" 
                         and "n = length((γ⇩1 @ γ⇩2)↿ C⇘𝒱⇩1⇙)" 
          by auto
        from  "Suc.prems"(2) ‹α = γ⇩1 @ [c⇩1] @ γ⇩2› have "γ⇩1 ↿ C⇘𝒱⇩2⇙ = []" 
          by (simp add: projection_concatenation_commute)
        from  "Suc.prems"(1) ‹α = γ⇩1 @ [c⇩1] @ γ⇩2› 
        obtain β' where "β'=β @ [c] @ γ⇩1"
                    and "β' @ [c⇩1] @ γ⇩2 ∈ Tr⇘ES⇙"
          by auto
        from ‹β' @ [c⇩1] @ γ⇩2 ∈ Tr⇘ES⇙›  ‹γ⇩2 ↿C⇘𝒱⇩1⇙ = []› ‹c⇩1 ∈ C⇘𝒱⇩1⇙› 
        obtain γ⇩2'  β'' where " β'' @ γ⇩2' ∈ Tr⇘ES⇙"
                         and "γ⇩2' ↿ V⇘𝒱⇩1⇙ = γ⇩2 ↿ V⇘𝒱⇩1⇙"
                         and "γ⇩2' ↿C⇘𝒱⇩1⇙ =[]"
                         and "β'' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)" 
          using D_𝒱⇩1  unfolding D_def by force
        
        from  c_in_C⇩1 have "c ∈ V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙"
          by auto  
        moreover
        from  ‹β'' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)› ‹β'=β @ [c] @ γ⇩1›  
        have "β'' ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = (β @ [c] @ γ⇩1) ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)"
          by auto 
        ultimately   
        have "∃ β''' γ⇩1'. β''=β'''@ [c] @ γ⇩1' 
                           ∧ β'''  ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) 
                           ∧ γ⇩1'↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = γ⇩1 ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)" 
          using projection_split_arbitrary_element by fast
        then  
        obtain β''' γ⇩1' where "β''= β''' @ [c] @ γ⇩1'" 
                         and  "β'''  ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)"
                         and  "γ⇩1'↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = γ⇩1 ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)" 
          using projection_split_arbitrary_element  by auto 
        
        from ‹β'' @ γ⇩2' ∈ Tr⇘ES⇙› this(1)
        have "β''' @ [c] @ γ⇩1' @ γ⇩2' ∈ Tr⇘ES⇙"
          by simp    

        from ‹γ⇩2' ↿C⇘𝒱⇩1⇙ =[]› have "γ⇩2' ↿ C⇘𝒱⇩2⇙=[]"
          using C2_subset_C1 projection_on_subset by auto
        moreover
        from ‹γ⇩1 ↿ C⇘𝒱⇩2⇙ = []› ‹γ⇩1'↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = γ⇩1 ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)› 
        have "γ⇩1'↿ C⇘𝒱⇩2⇙ = []" using C2_subset_C1 V2_subset_V1 
          by (metis non_empty_projection_on_subset projection_subset_eq_from_superset_eq sup_commute)               
        ultimately
        have "(γ⇩1' @ γ⇩2')↿C⇘𝒱⇩2⇙ = []" 
          by (simp add: projection_concatenation_commute)
          
        from ‹γ⇩1'↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = γ⇩1 ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)› have "γ⇩1'↿C⇘𝒱⇩1⇙ = γ⇩1↿C⇘𝒱⇩1⇙" 
          using projection_subset_eq_from_superset_eq sup_commute by metis
        hence "length(γ⇩1'↿C⇘𝒱⇩1⇙) = length(γ⇩1↿C⇘𝒱⇩1⇙)" by simp
        moreover
        from ‹γ⇩2 ↿C⇘𝒱⇩1⇙ = []› ‹γ⇩2'↿C⇘𝒱⇩1⇙=[]› have "length(γ⇩2'↿C⇘𝒱⇩1⇙) = length(γ⇩2↿C⇘𝒱⇩1⇙)"
          by simp
        ultimately
        have "n=length((γ⇩1' @ γ⇩2')↿C⇘𝒱⇩1⇙)" 
          by (simp add: ‹n = length ((γ⇩1 @ γ⇩2) ↿ C⇘𝒱⇩1⇙)› projection_concatenation_commute)

          
      
        from ‹β''' @ [c] @ γ⇩1' @ γ⇩2' ∈ Tr⇘ES⇙› ‹(γ⇩1' @ γ⇩2')↿C⇘𝒱⇩2⇙ = []› ‹n=length((γ⇩1' @ γ⇩2')↿C⇘𝒱⇩1⇙)› 
        have witness: 
        " ∃α' β'. β' @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩2⇙ = ( γ⇩1' @ γ⇩2')  ↿ V⇘𝒱⇩2⇙ 
                    ∧ α' ↿ C⇘𝒱⇩2⇙ = [] ∧ β' ↿ (V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) = β''' ↿ (V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙)" 
          using Suc.hyps[OF ‹β''' @ [c] @ γ⇩1' @ γ⇩2' ∈ Tr⇘ES⇙›] by simp
        
        from V⇩2_union_C⇩2_subset_V⇩1_union_C⇩1  ‹β'''  ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)› 
        have "β'''  ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) = β ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙)"
          using non_empty_projection_on_subset by blast
          
        from  𝒱⇩1IsViewOnE 𝒱⇩2IsViewOnE V2_subset_V1 C2_subset_C1  c⇩1_in_C⇩1 have "c⇩1 ∉ V⇘𝒱⇩2⇙"  
          unfolding isViewOn_def V_valid_def  VC_disjoint_def by auto
        with ‹α = γ⇩1 @ [c⇩1] @ γ⇩2› have "α ↿ V⇘𝒱⇩2⇙ = (γ⇩1 @ γ⇩2) ↿ V⇘𝒱⇩2⇙"
          unfolding projection_def by auto
        moreover
        from V2_subset_V1 ‹γ⇩2' ↿ V⇘𝒱⇩1⇙ = γ⇩2 ↿ V⇘𝒱⇩1⇙› have "γ⇩2' ↿ V⇘𝒱⇩2⇙ = γ⇩2 ↿ V⇘𝒱⇩2⇙"
           using V2_subset_V1 by (metis projection_subset_eq_from_superset_eq subset_Un_eq)
        moreover
        from ‹γ⇩1'↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = γ⇩1 ↿(V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)› have "γ⇩1' ↿ V⇘𝒱⇩2⇙ = γ⇩1 ↿ V⇘𝒱⇩2⇙" 
          using V2_subset_V1 by (metis projection_subset_eq_from_superset_eq subset_Un_eq)
        ultimately  
        have "α ↿ V⇘𝒱⇩2⇙ = (γ⇩1' @ γ⇩2') ↿ V⇘𝒱⇩2⇙" using ‹α ↿ V⇘𝒱⇩2⇙ = (γ⇩1 @ γ⇩2) ↿ V⇘𝒱⇩2⇙›
          by (simp add: projection_concatenation_commute)

        from ‹β'''  ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) = β ↿(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙)› ‹α ↿ V⇘𝒱⇩2⇙ = (γ⇩1' @ γ⇩2') ↿ V⇘𝒱⇩2⇙›
        show ?case
          using witness by simp
     qed          
 }  
  thus ?thesis
    unfolding D_def by auto 
qed
end 

context BSPTaxonomyDifferentViewsSecondDim
begin
(* lemma taken from lemma 3.5.5 from Heiko Mantel's dissertation*)
lemma FCD_implies_FCD_for_modified_view_gamma: 
"⟦FCD Γ⇩1 𝒱⇩1 Tr⇘ES⇙; 
     V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆  V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙;  N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇  N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙;  C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆  C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙ ⟧
     ⟹ FCD Γ⇩2 𝒱⇩2 Tr⇘ES⇙" 
proof -
  assume "FCD Γ⇩1 𝒱⇩1 Tr⇘ES⇙"
     and "V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆  V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙"
     and "N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇  N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙" 
     and "C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆  C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙"
  {
    fix α β v c
    assume "c ∈ C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙"
       and "v ∈ V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙"
       and "β @ [c,v] @ α ∈ Tr⇘ES⇙"
       and "α↿C⇘𝒱⇩2⇙ = []"
    
    from ‹c ∈ C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙› ‹C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆  C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙› have "c ∈  C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙"
      by auto
    moreover
    from ‹v ∈ V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙› ‹V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆  V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙› have "v ∈  V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙"
      by auto
    moreover
    from C2_equals_C1 ‹α↿C⇘𝒱⇩2⇙ = []› have "α↿C⇘𝒱⇩1⇙ = []"
      by auto
    ultimately
    obtain α' δ' where "(set δ') ⊆ (N⇘𝒱⇩1⇙ ∩ Δ⇘Γ⇩1⇙)"
                  and "β @ δ' @ [v] @ α' ∈ Tr⇘ES⇙"
                  and "α'↿V⇘𝒱⇩1⇙ = α↿V⇘𝒱⇩1⇙"
                  and "α'↿C⇘𝒱⇩1⇙ = []"
      using ‹β @ [c,v] @ α ∈ Tr⇘ES⇙› ‹FCD Γ⇩1 𝒱⇩1 Tr⇘ES⇙› unfolding FCD_def by blast  
    
    from ‹(set δ') ⊆ (N⇘𝒱⇩1⇙ ∩ Δ⇘Γ⇩1⇙)› ‹N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇  N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙› 
    have "(set δ') ⊆ (N⇘𝒱⇩2⇙ ∩ Δ⇘Γ⇩2⇙)"
      by auto
    moreover
    from ‹α'↿V⇘𝒱⇩1⇙ = α↿V⇘𝒱⇩1⇙› V2_subset_V1 have "α'↿V⇘𝒱⇩2⇙ = α↿V⇘𝒱⇩2⇙" 
    using non_empty_projection_on_subset by blast
    moreover
    from C2_equals_C1 ‹α'↿C⇘𝒱⇩1⇙ = []› have "α'↿C⇘𝒱⇩2⇙ = []"
      by auto
    ultimately
    have "∃ δ' α'. (set δ') ⊆ (N⇘𝒱⇩2⇙ ∩ Δ⇘Γ⇩2⇙) 
                         ∧ β @ δ'@ [v] @ α' ∈ Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇩2⇙ = α↿V⇘𝒱⇩2⇙ ∧ α'↿C⇘𝒱⇩2⇙ = []"
      using ‹β @ δ' @ [v] @ α' ∈ Tr⇘ES⇙› by auto                
  }
  thus ?thesis
    unfolding FCD_def by blast
qed  

(* lemma taken from lemma 3.5.10 in Heiko Mantel's dissertation*)
lemma SI_implies_SI_for_modified_view : 
"SI 𝒱⇩1 Tr⇘ES⇙ ⟹ SI 𝒱⇩2 Tr⇘ES⇙"
proof -
  assume  SI: "SI 𝒱⇩1 Tr⇘ES⇙"
  {
    fix α β c
    assume "c ∈ C⇘𝒱⇩2⇙"
      and  "β @ α ∈ Tr⇘ES⇙"
      and  alpha_C⇩2_empty: "α ↿ C⇘𝒱⇩2⇙ = []"
    moreover
    with  C2_equals_C1 have "c ∈ C⇘𝒱⇩1⇙"
      by auto  
    moreover
    from   alpha_C⇩2_empty C2_equals_C1 have "α ↿ C⇘𝒱⇩1⇙ = []"
      by auto
    ultimately
    have "β @ (c # α) ∈ Tr⇘ES⇙"
      using SI  unfolding SI_def by auto
  }
  thus ?thesis
    unfolding SI_def by auto  
qed  


(* lemma taken from lemma 3.5.10 in Heiko Mantel's dissertation*)
lemma BSI_implies_BSI_for_modified_view : 
"BSI 𝒱⇩1 Tr⇘ES⇙ ⟹ BSI 𝒱⇩2 Tr⇘ES⇙"
proof -
  assume  BSI: "BSI 𝒱⇩1 Tr⇘ES⇙"
  {
    fix α β c
    assume "c ∈ C⇘𝒱⇩2⇙"
      and  "β @ α ∈ Tr⇘ES⇙"
      and  alpha_C⇩2_empty: "α ↿ C⇘𝒱⇩2⇙ = []"
    moreover
    with  C2_equals_C1 have "c ∈ C⇘𝒱⇩1⇙"
      by auto  
    moreover
    from   alpha_C⇩2_empty C2_equals_C1 have "α ↿ C⇘𝒱⇩1⇙ = []"
      by auto
    ultimately
    have "∃ α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙ ∧ α' ↿ C⇘𝒱⇩1⇙ = []" 
      using BSI  unfolding BSI_def by auto
    with V2_subset_V1  C2_equals_C1
    have "∃ α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩2⇙ = α ↿ V⇘𝒱⇩2⇙ ∧ α' ↿ C⇘𝒱⇩2⇙ = []" 
      using non_empty_projection_on_subset by metis
  }
  thus ?thesis
    unfolding BSI_def by auto  
qed  

(* lemma taken from lemma 3.5.10 in Heiko Mantel's dissertation*)
lemma I_implies_I_for_modified_view : 
"I 𝒱⇩1 Tr⇘ES⇙ ⟹ I 𝒱⇩2 Tr⇘ES⇙"
proof -
  assume  I: "I 𝒱⇩1 Tr⇘ES⇙"
  from V2_subset_V1 C2_equals_C1 have V⇩2_union_C⇩2_subset_V⇩1_union_C⇩1: "V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙ ⊆ V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙"
    by auto
  {
    fix α β c
    assume "c ∈ C⇘𝒱⇩2⇙"
      and  "β @ α ∈ Tr⇘ES⇙"
      and  alpha_C⇩2_empty: "α ↿ C⇘𝒱⇩2⇙ = []"
    moreover
    with C2_equals_C1 have "c ∈ C⇘𝒱⇩1⇙"
      by auto  
    moreover
    from   alpha_C⇩2_empty C2_equals_C1 have "α ↿ C⇘𝒱⇩1⇙ = []" 
      by auto
    ultimately
    have "∃ α' β'. 
            β' @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙ ∧ α' ↿ C⇘𝒱⇩1⇙ = [] 
              ∧ β' ↿ (V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿ (V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)" 
      using I  unfolding I_def by auto
    with  V⇩2_union_C⇩2_subset_V⇩1_union_C⇩1 V2_subset_V1  C2_equals_C1
    have "∃ α' β'. 
              β' @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩2⇙ = α ↿ V⇘𝒱⇩2⇙ ∧ α' ↿ C⇘𝒱⇩2⇙ = []  
                ∧ β' ↿ (V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) = β ↿ (V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙)" 
      using non_empty_projection_on_subset by metis
  }
  thus ?thesis
    unfolding I_def by auto  
qed  

(* lemma taken from lemma 3.5.10 in Heiko Mantel's dissertation*)
lemma SIA_implies_SIA_for_modified_view : 
"⟦SIA ρ⇩1 𝒱⇩1 Tr⇘ES⇙; ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1) ⟧ ⟹ SIA ρ⇩2 𝒱⇩2 Tr⇘ES⇙"
proof -
  assume  SIA: "SIA ρ⇩1 𝒱⇩1 Tr⇘ES⇙"
    and   ρ⇩2_supseteq_ρ⇩1: "ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1)" 
  {
    fix α β c
    assume "c ∈ C⇘𝒱⇩2⇙"
      and  "β @ α ∈ Tr⇘ES⇙"
      and  alpha_C⇩2_empty: "α ↿ C⇘𝒱⇩2⇙ = []"
      and admissible_c_ρ⇩2_𝒱⇩2:"Adm 𝒱⇩2 ρ⇩2 Tr⇘ES⇙ β c"
    moreover
    with  C2_equals_C1 have "c ∈ C⇘𝒱⇩1⇙"
      by auto  
    moreover
    from   alpha_C⇩2_empty C2_equals_C1 have "α ↿ C⇘𝒱⇩1⇙ = []"
      by auto
    moreover
    from ρ⇩2_supseteq_ρ⇩1  admissible_c_ρ⇩2_𝒱⇩2 have "Adm 𝒱⇩1 ρ⇩1 Tr⇘ES⇙ β c" 
      by (simp add: Adm_implies_Adm_for_modified_rho)
    ultimately
    have "β @ (c # α) ∈ Tr⇘ES⇙"
      using SIA  unfolding SIA_def by auto
  }
  thus ?thesis
    unfolding SIA_def by auto  
qed  


(* lemma taken from lemma 3.5.10 in Heiko Mantel's dissertation*)
lemma BSIA_implies_BSIA_for_modified_view : 
"⟦BSIA ρ⇩1 𝒱⇩1 Tr⇘ES⇙; ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1) ⟧ ⟹ BSIA ρ⇩2 𝒱⇩2 Tr⇘ES⇙"
proof -
  assume  BSIA: "BSIA ρ⇩1 𝒱⇩1 Tr⇘ES⇙"
    and   ρ⇩2_supseteq_ρ⇩1: "ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1)" 
  from V2_subset_V1 C2_equals_C1
  have V⇩2_union_C⇩2_subset_V⇩1_union_C⇩1: "V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙ ⊆ V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙"
    by auto
  {
    fix α β c
    assume "c ∈ C⇘𝒱⇩2⇙"
      and  "β @ α ∈ Tr⇘ES⇙"
      and  alpha_C⇩2_empty: "α ↿ C⇘𝒱⇩2⇙ = []"
      and admissible_c_ρ⇩2_𝒱⇩2:"Adm 𝒱⇩2 ρ⇩2 Tr⇘ES⇙ β c"
    moreover
    with  C2_equals_C1 have "c ∈ C⇘𝒱⇩1⇙"
      by auto  
    moreover
    from   alpha_C⇩2_empty C2_equals_C1 have "α ↿ C⇘𝒱⇩1⇙ = []"
      by auto
    moreover
    from ρ⇩2_supseteq_ρ⇩1  admissible_c_ρ⇩2_𝒱⇩2 have "Adm 𝒱⇩1 ρ⇩1 Tr⇘ES⇙ β c"
      by (simp add: Adm_implies_Adm_for_modified_rho)
    ultimately
    have "∃ α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙ ∧ α' ↿ C⇘𝒱⇩1⇙ = []" 
      using BSIA  unfolding BSIA_def by auto
    with V2_subset_V1  C2_equals_C1 
    have "∃ α'. β @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩2⇙ = α ↿ V⇘𝒱⇩2⇙ ∧ α' ↿ C⇘𝒱⇩2⇙ = []" 
      using non_empty_projection_on_subset by metis
  }
  thus ?thesis
    unfolding BSIA_def by auto  
qed  

(* lemma taken from lemma 3.5.10 in Heiko Mantel's dissertation*)
lemma IA_implies_IA_for_modified_view : 
"⟦IA ρ⇩1 𝒱⇩1 Tr⇘ES⇙; ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1) ⟧ ⟹ IA ρ⇩2 𝒱⇩2 Tr⇘ES⇙"
proof -
  assume  IA: "IA ρ⇩1 𝒱⇩1 Tr⇘ES⇙"
    and   ρ⇩2_supseteq_ρ⇩1: "ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1)" 
  {
    fix α β c
    assume "c ∈ C⇘𝒱⇩2⇙"
      and  "β @ α ∈ Tr⇘ES⇙"
      and  alpha_C⇩2_empty: "α ↿ C⇘𝒱⇩2⇙ = []"
      and admissible_c_ρ⇩2_𝒱⇩2:"Adm 𝒱⇩2 ρ⇩2 Tr⇘ES⇙ β c"
    moreover
    with C2_equals_C1 have "c ∈ C⇘𝒱⇩1⇙"
      by auto  
    moreover
    from   alpha_C⇩2_empty C2_equals_C1 have "α ↿ C⇘𝒱⇩1⇙ = []"
      by auto
    moreover
    from ρ⇩2_supseteq_ρ⇩1  admissible_c_ρ⇩2_𝒱⇩2 have "Adm 𝒱⇩1 ρ⇩1 Tr⇘ES⇙ β c"
      by (simp add: Adm_implies_Adm_for_modified_rho)
    ultimately
    have "∃ α' β'. β' @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩1⇙ = α ↿ V⇘𝒱⇩1⇙ ∧ α' ↿ C⇘𝒱⇩1⇙ = [] ∧ β' ↿ (V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙) = β ↿ (V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)" 
      using IA  unfolding IA_def by auto
    moreover
    from   V2_subset_V1 C2_equals_C1 have "(V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) ⊆  (V⇘𝒱⇩1⇙ ∪ C⇘𝒱⇩1⇙)"
      by auto 
    ultimately
    have "∃ α' β'. β' @ [c] @ α' ∈ Tr⇘ES⇙ ∧ α' ↿ V⇘𝒱⇩2⇙ = α ↿ V⇘𝒱⇩2⇙ ∧ α' ↿ C⇘𝒱⇩2⇙ = []  ∧ β' ↿ (V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙) = β ↿ (V⇘𝒱⇩2⇙ ∪ C⇘𝒱⇩2⇙)" 
      using V2_subset_V1  C2_equals_C1   non_empty_projection_on_subset by metis
  }
  thus ?thesis
    unfolding IA_def by auto  
qed

(* lemma taken from lemma 3.5.14 from Heiko Mantel's dissertation*)
lemma FCI_implies_FCI_for_modified_view_gamma: 
"⟦FCI Γ⇩1 𝒱⇩1 Tr⇘ES⇙;
     V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆  V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙;  N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇  N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙;  C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆  C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙ ⟧
     ⟹ FCI Γ⇩2 𝒱⇩2 Tr⇘ES⇙" 
proof -
  assume "FCI Γ⇩1 𝒱⇩1 Tr⇘ES⇙"
     and "V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆  V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙"
     and "N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇  N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙" 
     and "C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆  C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙"
  {
    fix α β v c
    assume "c ∈ C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙"
       and "v ∈ V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙"
       and "β @ [v] @ α ∈ Tr⇘ES⇙"
       and "α↿C⇘𝒱⇩2⇙ = []"
    
    from ‹c ∈ C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙› ‹C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆  C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙› have "c ∈  C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙"
      by auto
    moreover
    from ‹v ∈ V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙› ‹V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆  V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙› have "v ∈  V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙"
      by auto
    moreover
    from C2_equals_C1 ‹α↿C⇘𝒱⇩2⇙ = []› have "α↿C⇘𝒱⇩1⇙ = []"
      by auto
    ultimately 
    obtain α' δ' where "(set δ') ⊆ (N⇘𝒱⇩1⇙ ∩ Δ⇘Γ⇩1⇙)"
                  and "β @ [c] @ δ' @ [v] @ α' ∈ Tr⇘ES⇙"
                  and "α'↿V⇘𝒱⇩1⇙ = α↿V⇘𝒱⇩1⇙"
                  and "α'↿C⇘𝒱⇩1⇙ = []"
      using ‹β @ [v] @ α ∈ Tr⇘ES⇙› ‹FCI Γ⇩1 𝒱⇩1 Tr⇘ES⇙› unfolding FCI_def by blast  
    
    from ‹(set δ') ⊆ (N⇘𝒱⇩1⇙ ∩ Δ⇘Γ⇩1⇙)› ‹N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇  N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙› 
    have "(set δ') ⊆ (N⇘𝒱⇩2⇙ ∩ Δ⇘Γ⇩2⇙)"
      by auto
    moreover
    from ‹α'↿V⇘𝒱⇩1⇙ = α↿V⇘𝒱⇩1⇙› V2_subset_V1 have "α'↿V⇘𝒱⇩2⇙ = α↿V⇘𝒱⇩2⇙" 
      using non_empty_projection_on_subset by blast
    moreover
    from ‹C⇘𝒱⇩2⇙ = C⇘𝒱⇩1⇙› ‹α'↿C⇘𝒱⇩1⇙ = []› have "α'↿C⇘𝒱⇩2⇙ = []"
      by auto
    ultimately have "∃ δ' α'. (set δ') ⊆ (N⇘𝒱⇩2⇙ ∩ Δ⇘Γ⇩2⇙) 
                         ∧ β @ [c] @  δ'@ [v] @ α' ∈ Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇩2⇙ = α↿V⇘𝒱⇩2⇙ ∧ α'↿C⇘𝒱⇩2⇙ = []"
               using ‹β @ [c] @ δ' @ [v] @ α' ∈ Tr⇘ES⇙› by auto                
  }
  thus ?thesis
    unfolding FCI_def by blast
qed  


(* lemma taken from lemma 3.5.14 from Heiko Mantel's dissertation*)
lemma FCIA_implies_FCIA_for_modified_view_rho_gamma: 
"⟦FCIA ρ⇩1 Γ⇩1 𝒱⇩1 Tr⇘ES⇙; ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1);
     V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆  V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙;  N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇  N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙;  C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆  C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙ ⟧
     ⟹ FCIA ρ⇩2 Γ⇩2 𝒱⇩2 Tr⇘ES⇙" 
proof -
  assume "FCIA ρ⇩1 Γ⇩1 𝒱⇩1 Tr⇘ES⇙"
     and "ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1)"
     and "V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆  V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙"
     and "N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇  N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙" 
     and "C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆  C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙"
  {
    fix α β v c
    assume "c ∈ C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙"
       and "v ∈ V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙"
       and "β @ [v] @ α ∈ Tr⇘ES⇙"
       and "α↿C⇘𝒱⇩2⇙ = []"
       and "Adm 𝒱⇩2 ρ⇩2 Tr⇘ES⇙ β c"
    
    from ‹c ∈ C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙› ‹C⇘𝒱⇩2⇙∩Υ⇘Γ⇩2⇙ ⊆  C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙› have "c ∈  C⇘𝒱⇩1⇙∩Υ⇘Γ⇩1⇙"
      by auto
    moreover
    from ‹v ∈ V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙› ‹V⇘𝒱⇩2⇙∩∇⇘Γ⇩2⇙ ⊆  V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙› have "v ∈  V⇘𝒱⇩1⇙∩∇⇘Γ⇩1⇙"
      by auto
    moreover
    from C2_equals_C1 ‹α↿C⇘𝒱⇩2⇙ = []› have "α↿C⇘𝒱⇩1⇙ = []"
      by auto
    moreover
    from ‹Adm 𝒱⇩2 ρ⇩2 Tr⇘ES⇙ β c› ‹ρ⇩2(𝒱⇩2) ⊇ ρ⇩1(𝒱⇩1)› have "Adm 𝒱⇩1 ρ⇩1 Tr⇘ES⇙ β c" 
       by (simp add: Adm_implies_Adm_for_modified_rho)
    ultimately
    obtain α' δ' where "(set δ') ⊆ (N⇘𝒱⇩1⇙ ∩ Δ⇘Γ⇩1⇙)"
                  and "β @ [c] @ δ' @ [v] @ α' ∈ Tr⇘ES⇙"
                  and "α'↿V⇘𝒱⇩1⇙ = α↿V⇘𝒱⇩1⇙"
                  and "α'↿C⇘𝒱⇩1⇙ = []"
      using ‹β @ [v] @ α ∈ Tr⇘ES⇙› ‹FCIA ρ⇩1 Γ⇩1 𝒱⇩1 Tr⇘ES⇙› unfolding FCIA_def by blast  
    
    from ‹(set δ') ⊆ (N⇘𝒱⇩1⇙ ∩ Δ⇘Γ⇩1⇙)› ‹N⇘𝒱⇩2⇙∩Δ⇘Γ⇩2⇙ ⊇  N⇘𝒱⇩1⇙∩Δ⇘Γ⇩1⇙› 
    have "(set δ') ⊆ (N⇘𝒱⇩2⇙ ∩ Δ⇘Γ⇩2⇙)"
      by auto
    moreover
    from ‹α'↿V⇘𝒱⇩1⇙ = α↿V⇘𝒱⇩1⇙› V2_subset_V1 have "α'↿V⇘𝒱⇩2⇙ = α↿V⇘𝒱⇩2⇙" 
      using non_empty_projection_on_subset by blast
    moreover
    from ‹C⇘𝒱⇩2⇙ = C⇘𝒱⇩1⇙› ‹α'↿C⇘𝒱⇩1⇙ = []› have "α'↿C⇘𝒱⇩2⇙ = []"
      by auto
    ultimately
    have "∃ δ' α'. (set δ') ⊆ (N⇘𝒱⇩2⇙ ∩ Δ⇘Γ⇩2⇙) 
                         ∧ β @ [c] @  δ'@ [v] @ α' ∈ Tr⇘ES⇙ ∧ α'↿V⇘𝒱⇩2⇙ = α↿V⇘𝒱⇩2⇙ ∧ α'↿C⇘𝒱⇩2⇙ = []"
      using ‹β @ [c] @ δ' @ [v] @ α' ∈ Tr⇘ES⇙› by auto                
  }
  thus ?thesis
    unfolding FCIA_def by blast
qed   
end

end