Theory UnwindingResults

theory UnwindingResults
imports AuxiliaryLemmas
begin

context Unwinding
begin
theorem unwinding_theorem_BSD:
"⟦ lrf ur; osc ur ⟧ ⟹ BSD 𝒱 Tr⇘(induceES SES)⇙"
proof -
  assume lrf_true: "lrf ur"
  assume osc_true: "osc ur"

  { (* show that the conclusion of the BSP follows from the assumptions *)
    fix α β c
    assume c_in_C: "c ∈ C⇘𝒱⇙"
    assume βcα_in_Tr: "((β @ [c]) @ α) ∈ Tr⇘(induceES SES)⇙"
    assume α_contains_no_c: "α ↿ C⇘𝒱⇙ = []"
 
    from state_from_induceES_trace[OF βcα_in_Tr] obtain s1'
      where s1'_in_S: "s1' ∈ S⇘SES⇙" 
      and enabled_s1'_α: "enabled SES s1' α" 
      and s0_βc_s1': "s0⇘SES⇙ (β @ [c])⟹⇘SES⇙ s1'"
      and reachable_s1': "reachable SES s1'"
      by auto
    
    from path_split_single2[OF s0_βc_s1'] obtain s1
      where s1_in_S: "s1 ∈ S⇘SES⇙" 
      and s0_β_s1: "s0⇘SES⇙ β⟹⇘SES⇙ s1" 
      and s1_c_s1': "s1 c⟶⇘SES⇙ s1'"
      and reachable_s1: "reachable SES s1"
      by auto

    from s1_in_S s1'_in_S c_in_C reachable_s1 s1_c_s1' lrf_true 
    have s1'_ur_s1: "((s1', s1) ∈ ur)"
      by (simp add: lrf_def, auto)

    from osc_property[OF osc_true s1_in_S s1'_in_S α_contains_no_c reachable_s1
      reachable_s1' enabled_s1'_α s1'_ur_s1]
    obtain α' 
      where α'_contains_no_c: "α' ↿ C⇘𝒱⇙ = []"
      and α'_V_is_α_V: "α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙"
      and enabled_s1_α': "enabled SES s1 α'" 
      by auto
  
    have βα'_in_Tr: "β @ α' ∈ Tr⇘(induceES SES)⇙"
    proof -
      note s0_β_s1
      moreover
      from enabled_s1_α' obtain s2
        where "s1 α'⟹⇘SES⇙ s2"
        by (simp add: enabled_def, auto)
      ultimately have "s0⇘SES⇙ (β @ α') ⟹⇘SES⇙ s2"
        by (rule path_trans)
      thus ?thesis
        by (simp add: induceES_def possible_traces_def enabled_def)
    qed
    
    from βα'_in_Tr α'_V_is_α_V α'_contains_no_c have 
      "∃α'. ((β @ α') ∈ (Tr⇘(induceES SES)⇙) ∧ (α' ↿ (V⇘𝒱⇙)) = (α ↿ V⇘𝒱⇙) ∧ α' ↿ C⇘𝒱⇙ = [])"
      by auto
  }
  thus ?thesis 
    by (simp add: BSD_def) 
qed

theorem unwinding_theorem_BSI:
"⟦ lrb ur; osc ur ⟧ ⟹ BSI 𝒱 Tr⇘(induceES SES)⇙"
proof -
  assume lrb_true: "lrb ur"
  assume osc_true: "osc ur"
  
  {   (* show that the conclusion of the BSP follows from the assumptions *)
    fix α β c
    assume c_in_C: "c ∈ C⇘𝒱⇙"
    assume βα_in_ind_Tr: "(β @ α) ∈ Tr⇘(induceES SES)⇙"
    assume α_contains_no_c: "α ↿ C⇘𝒱⇙ = []"
    
    from state_from_induceES_trace[OF βα_in_ind_Tr] obtain s1
      where s1_in_S : "s1 ∈ S⇘SES⇙"
      and path_β_yields_s1:  "s0⇘SES⇙ β⟹⇘SES⇙ s1" 
      and enabled_s1_α: "enabled SES s1 α"
      and reachable_s1: "reachable SES s1"
      by auto

    from reachable_s1 s1_in_S c_in_C  lrb_true 
    have "∃s1'∈ S⇘SES⇙. s1 c⟶⇘SES⇙ s1' ∧ (s1, s1') ∈ ur"
      by(simp add: lrb_def) 
    then obtain s1' 
      where s1'_in_S: "s1' ∈ S⇘SES⇙"
      and s1_trans_c_s1': "s1 c⟶⇘SES⇙ s1'"
      and s1_s1'_in_ur: "(s1, s1') ∈ ur" 
      by auto

    have reachable_s1': "reachable SES s1'" 
    proof -
      from path_β_yields_s1 s1_trans_c_s1' have "s0⇘SES⇙ (β @ [c])⟹⇘SES⇙ s1'"
        by (rule path_trans_single)
      thus ?thesis by (simp add: reachable_def, auto)
    qed
    
    from osc_property[OF osc_true s1'_in_S s1_in_S α_contains_no_c 
      reachable_s1' reachable_s1 enabled_s1_α s1_s1'_in_ur]
    obtain α' 
      where α'_contains_no_c: "α' ↿ C⇘𝒱⇙ = []"
      and α'_V_is_α_V: "α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙"
      and enabled_s1'_α': "enabled SES s1' α'" 
      by auto

    have βcα'_in_ind_Tr: "β @ [c] @ α' ∈ Tr⇘(induceES SES)⇙"
    proof -
      from path_β_yields_s1 s1_trans_c_s1' have "s0⇘SES⇙ (β @ [c])⟹⇘SES⇙ s1'"
        by (rule path_trans_single)
      moreover
      from enabled_s1'_α' obtain s2
        where "s1' α'⟹⇘SES⇙ s2"
        by (simp add: enabled_def, auto)
      ultimately have "s0⇘SES⇙ ((β @ [c]) @ α')⟹⇘SES⇙ s2"
        by (rule path_trans)
      thus ?thesis
        by (simp add: induceES_def possible_traces_def enabled_def)
    qed
    
    from βcα'_in_ind_Tr α'_V_is_α_V α'_contains_no_c 
    have "∃α'. β @ c # α' ∈ Tr⇘(induceES SES)⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []"
      by auto
  }
  thus ?thesis
    by(simp add: BSI_def)
qed

(* unwinding theorem for BSP BSIA *)
theorem unwinding_theorem_BSIA:
"⟦ lrbe ρ ur; osc ur ⟧ ⟹ BSIA ρ 𝒱 Tr⇘(induceES SES)⇙"
proof -
  assume lrbe_true: "lrbe ρ ur"
  assume osc_true: "osc ur"
  
  { (* show that the conclusion of the BSP follows from the assumptions *)
    fix α β c
    assume c_in_C: "c ∈ C⇘𝒱⇙"
    assume βα_in_ind_Tr: "(β @ α) ∈ Tr⇘(induceES SES)⇙"
    assume α_contains_no_c: "α ↿ C⇘𝒱⇙ = []"
    
    assume adm: "Adm 𝒱 ρ Tr⇘(induceES SES)⇙ β c"
    
    from state_from_induceES_trace[OF βα_in_ind_Tr] 
    obtain s1 
      where s1_in_S : "s1 ∈ S⇘SES⇙"
      and s0_β_s1:  "s0⇘SES⇙ β⟹⇘SES⇙ s1" 
      and enabled_s1_α: "enabled SES s1 α"  
      and reachable_s1: "reachable SES s1"
      by auto

        (* case distinction whether En is true or not *)
    have "∃α'. β @ [c] @ α' ∈ Tr⇘(induceES SES)⇙ ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []"
    proof cases
      assume en: "En ρ s1 c" (*first case, en is true *)

      from reachable_s1 s1_in_S c_in_C en lrbe_true 
      have "∃s1'∈ S⇘SES⇙. s1 c⟶⇘SES⇙ s1' ∧ (s1, s1') ∈ ur"
        by(simp add: lrbe_def) 
      then obtain s1' 
        where s1'_in_S: "s1' ∈ S⇘SES⇙"
        and s1_trans_c_s1': "s1 c⟶⇘SES⇙ s1'"
        and s1_s1'_in_ur: "(s1, s1') ∈ ur" 
        by auto

      have reachable_s1': "reachable SES s1'" 
      proof -
        from s0_β_s1 s1_trans_c_s1' have "s0⇘SES⇙ (β @ [c])⟹⇘SES⇙ s1'"
          by (rule path_trans_single)
        thus ?thesis by (simp add: reachable_def, auto)
      qed 

      from osc_property[OF osc_true s1'_in_S s1_in_S α_contains_no_c 
        reachable_s1' reachable_s1 enabled_s1_α s1_s1'_in_ur] 
      obtain α' 
        where α'_contains_no_c: "α' ↿ C⇘𝒱⇙ = []"
        and α'_V_is_α_V: "α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙"
        and enabled_s1'_α': "enabled SES s1' α'" 
        by auto
      
      have βcα'_in_ind_Tr: "β @ [c] @ α' ∈ Tr⇘(induceES SES)⇙"
      proof -
        from s0_β_s1 s1_trans_c_s1' have "s0⇘SES⇙ (β @ [c])⟹⇘SES⇙ s1'"
          by (rule path_trans_single)
        moreover
        from enabled_s1'_α' obtain s2
          where "s1' α'⟹⇘SES⇙ s2"
          by (simp add: enabled_def, auto)
        ultimately have "s0⇘SES⇙ ((β @ [c]) @ α')⟹⇘SES⇙ s2"
          by (rule path_trans)
        thus ?thesis
          by (simp add: induceES_def possible_traces_def enabled_def)
      qed
      
      from βcα'_in_ind_Tr α'_V_is_α_V α'_contains_no_c show ?thesis
        by auto
    next (* second case, en is false *)
      assume not_en: "¬ En ρ s1 c"
      
      let ?A = "(Adm 𝒱 ρ (Tr⇘(induceES SES)⇙) β c)"
      let ?E = "∃s ∈ S⇘SES⇙. (s0⇘SES⇙ β⟹⇘SES⇙ s ∧ En ρ s c)"

      { (* show the contraposition of Adm_to_En *)
        assume adm: "?A" 
        
        from s0_β_s1 have β_in_Tr: "β ∈ Tr⇘(induceES SES)⇙"
          by (simp add: induceES_def possible_traces_def enabled_def)
        
        from  β_in_Tr adm have "?E"
          by (rule Adm_to_En)
      }
      hence Adm_to_En_contr: "¬ ?E ⟹ ¬ ?A"
        by blast
      with s1_in_S s0_β_s1 not_en have not_adm: "¬ ?A"
        by auto
      with adm show ?thesis
        by auto
    qed
  }
  thus ?thesis 
    by (simp add: BSIA_def)
qed

theorem unwinding_theorem_FCD:
"⟦ fcrf Γ ur; osc ur ⟧ ⟹ FCD Γ 𝒱 Tr⇘(induceES SES)⇙"
proof - 
  assume fcrf: "fcrf Γ ur"
  assume osc: "osc ur"

  { (* show that the conclusion of the BSP follows from the assumptions *)
    fix α β c v

    assume c_in_C_inter_Y: "c ∈ (C⇘𝒱⇙ ∩ Υ⇘Γ⇙)"
    assume v_in_V_inter_Nabla: "v ∈ (V⇘𝒱⇙ ∩ ∇⇘Γ⇙)"
    assume βcvα_in_Tr: "((β @ [c] @ [v]) @ α) ∈ Tr⇘(induceES SES)⇙"
    assume α_contains_no_c: "α ↿ C⇘𝒱⇙ = []"

    from state_from_induceES_trace[OF βcvα_in_Tr] obtain s1'
      where s1'_in_S: "s1' ∈ S⇘SES⇙"
      and s0_βcv_s1': "s0⇘SES⇙ (β @ ([c] @ [v]))⟹⇘SES⇙ s1'"
      and enabled_s1'_α: "enabled SES s1' α"
      and reachable_s1': "reachable SES s1'"
      by auto
    
    from path_split2[OF s0_βcv_s1'] obtain s1 
      where s1_in_S: "s1 ∈ S⇘SES⇙"
      and s0_β_s1: "s0⇘SES⇙ β⟹⇘SES⇙ s1"
      and s1_cv_s1': "s1 ([c] @ [v])⟹⇘SES⇙ s1'"
      and reachable_s1: "reachable SES s1"
      by (auto)

    from c_in_C_inter_Y v_in_V_inter_Nabla s1_in_S s1'_in_S reachable_s1 s1_cv_s1' fcrf
    have "∃s1'' ∈ S⇘SES⇙. ∃δ. (∀d ∈ (set δ). d ∈ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙)) ∧
      s1 (δ @ [v])⟹⇘SES⇙ s1'' ∧ (s1', s1'') ∈ ur"
      by (simp add: fcrf_def)
    then obtain s1'' δ
      where s1''_in_S: "s1'' ∈ S⇘SES⇙"
      and δ_in_N_inter_Delta_star: "(∀d ∈ (set δ). d ∈ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙))"
      and s1_δv_s1'': "s1 (δ @ [v])⟹⇘SES⇙ s1''"
      and s1'_ur_s1'': "(s1', s1'') ∈ ur" 
      by auto
      
    have reachable_s1'': "reachable SES s1''"
    proof -
      from s0_β_s1 s1_δv_s1'' have "s0⇘SES⇙ (β @ (δ @ [v]))⟹⇘SES⇙ s1''"
        by (rule path_trans)
      thus ?thesis
        by (simp add: reachable_def, auto)
    qed

    from osc_property[OF  osc s1''_in_S s1'_in_S α_contains_no_c 
      reachable_s1'' reachable_s1' enabled_s1'_α s1'_ur_s1'']
    obtain α' 
      where  α'_contains_no_c: "α' ↿ C⇘𝒱⇙ = []"
      and α'_V_is_α_V: "α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙"
      and enabled_s1''_α': "enabled SES s1'' α'" 
      by auto

    have βδvα'_in_Tr: "β @ δ @ [v] @ α' ∈ Tr⇘(induceES SES)⇙"
      proof -
        from s0_β_s1 s1_δv_s1'' have "s0⇘SES⇙ (β @ δ @ [v])⟹⇘SES⇙ s1''"
          by (rule path_trans)
        moreover
        from enabled_s1''_α' obtain s2
          where "s1'' α'⟹⇘SES⇙ s2"
          by (simp add: enabled_def, auto)
        ultimately have "s0⇘SES⇙ ((β @ δ @ [v]) @ α')⟹⇘SES⇙ s2"
          by (rule path_trans)
        thus ?thesis
          by (simp add: induceES_def possible_traces_def enabled_def)
      qed

      from δ_in_N_inter_Delta_star βδvα'_in_Tr α'_V_is_α_V α'_contains_no_c
      have "∃α'. ∃δ'. set δ' ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ β @ δ' @ [v] @ α' ∈ Tr⇘(induceES SES)⇙ 
        ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []"
        by auto
  }
  thus ?thesis
    by (simp add: FCD_def)
qed

theorem unwinding_theorem_FCI:
"⟦ fcrb Γ ur; osc ur ⟧ ⟹ FCI Γ 𝒱 Tr⇘(induceES SES)⇙"
proof -
  assume fcrb: "fcrb Γ ur"
  assume osc: "osc ur"

  { (* show that the conclusion of the BSP follows from the assumptions *)
    fix α β c v

    assume c_in_C_inter_Y: "c ∈ (C⇘𝒱⇙ ∩ Υ⇘Γ⇙)"
    assume v_in_V_inter_Nabla: "v ∈ (V⇘𝒱⇙ ∩ ∇⇘Γ⇙)"
    assume βvα_in_Tr: "((β @ [v]) @ α) ∈ Tr⇘(induceES SES)⇙"
    assume α_contains_no_c: "α ↿ C⇘𝒱⇙ = []"
  
    from state_from_induceES_trace[OF βvα_in_Tr] obtain s1''
      where s1''_in_S: "s1'' ∈ S⇘SES⇙"
      and s0_βv_s1'': "s0⇘SES⇙ (β @ [v]) ⟹⇘SES⇙ s1''"
      and enabled_s1''_α: "enabled SES s1'' α"
      and reachable_s1'': "reachable SES s1''"
      by auto

    from path_split_single2[OF s0_βv_s1''] obtain s1 
      where s1_in_S: "s1 ∈ S⇘SES⇙"
      and s0_β_s1: "s0⇘SES⇙ β⟹⇘SES⇙ s1"
      and s1_v_s1'': "s1 v⟶⇘SES⇙ s1''"
      and reachable_s1: "reachable SES s1"
      by (auto)

    from c_in_C_inter_Y v_in_V_inter_Nabla s1_in_S 
      s1''_in_S reachable_s1 s1_v_s1'' fcrb 
    have "∃s1' ∈ S⇘SES⇙. ∃δ. (∀d ∈ (set δ). d ∈ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙))
      ∧ s1 ([c] @ δ @ [v])⟹⇘SES⇙ s1'
      ∧ (s1'', s1') ∈ ur"
      by (simp add: fcrb_def)
    then obtain s1' δ
      where s1'_in_S: "s1' ∈ S⇘SES⇙"
      and δ_in_N_inter_Delta_star: "(∀d ∈ (set δ). d ∈ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙))"
      and s1_cδv_s1': "s1 ([c] @ δ @ [v])⟹⇘SES⇙ s1'"
      and s1''_ur_s1': "(s1'', s1') ∈ ur" 
      by auto

    have reachable_s1': "reachable SES s1'"
    proof -
      from s0_β_s1 s1_cδv_s1' have "s0⇘SES⇙ (β @ ([c] @ δ @ [v]))⟹⇘SES⇙ s1'"
        by (rule path_trans)
      thus ?thesis
        by (simp add: reachable_def, auto)
    qed
    
    from osc_property[OF osc s1'_in_S s1''_in_S α_contains_no_c 
      reachable_s1' reachable_s1'' enabled_s1''_α s1''_ur_s1']
    obtain α' 
      where  α'_contains_no_c: "α' ↿ C⇘𝒱⇙ = []"
      and α'_V_is_α_V: "α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙"
      and enabled_s1'_α': "enabled SES s1' α'" 
      by auto

    have βcδvα'_in_Tr: "β @ [c] @ δ @ [v] @ α' ∈ Tr⇘(induceES SES)⇙"
    proof -
      let ?l1 = "β @ [c] @ δ @ [v]"
      let ?l2 = "α'"
      from s0_β_s1 s1_cδv_s1' have "s0⇘SES⇙ (?l1)⟹⇘SES⇙ s1'"
        by (rule path_trans)
      moreover
      from enabled_s1'_α' obtain s1337 where "s1' ?l2 ⟹⇘SES⇙ s1337"
        by (simp add: enabled_def, auto)
      ultimately have "s0⇘SES⇙ (?l1 @ ?l2)⟹⇘SES⇙ s1337"
        by (rule path_trans)
      thus ?thesis
        by (simp add: induceES_def possible_traces_def enabled_def) 
    qed

from δ_in_N_inter_Delta_star βcδvα'_in_Tr α'_V_is_α_V α'_contains_no_c
    have "∃α' δ'.
      set δ' ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ β @ [c] @ δ' @ [v] @ α' ∈ Tr⇘(induceES SES)⇙ 
      ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = []"
      by auto
  }
  thus ?thesis
    by(simp add: FCI_def)     
qed

theorem unwinding_theorem_FCIA:
"⟦ fcrbe Γ ρ ur; osc ur ⟧ ⟹ FCIA ρ Γ 𝒱 Tr⇘(induceES SES)⇙"
proof -
  assume fcrbe: "fcrbe Γ ρ ur"
  assume osc: "osc ur"

  { (* show that the conclusion of the BSP follows from the assumptions *)
    fix α β c v

    assume c_in_C_inter_Y: "c ∈ (C⇘𝒱⇙ ∩ Υ⇘Γ⇙)"
    assume v_in_V_inter_Nabla: "v ∈ (V⇘𝒱⇙ ∩ ∇⇘Γ⇙)"
    assume βvα_in_Tr: "((β @ [v]) @ α) ∈ Tr⇘(induceES SES)⇙"
    assume α_contains_no_c: "α ↿ C⇘𝒱⇙ = []"
    assume adm: "Adm 𝒱 ρ Tr⇘(induceES SES)⇙ β c"

    from state_from_induceES_trace[OF βvα_in_Tr] obtain s1''
      where s1''_in_S: "s1'' ∈ S⇘SES⇙"
      and s0_βv_s1'': "s0⇘SES⇙ (β @ [v])⟹⇘SES⇙ s1''"
      and enabled_s1''_α: "enabled SES s1'' α"
      and reachable_s1'': "reachable SES s1''"
      by auto

    from path_split_single2[OF s0_βv_s1''] obtain s1 
      where s1_in_S: "s1 ∈ S⇘SES⇙"
      and s0_β_s1: "s0⇘SES⇙ β⟹⇘SES⇙ s1"
      and s1_v_s1'': "s1 v⟶⇘SES⇙ s1''"
      and reachable_s1: "reachable SES s1"
      by (auto)
    
    have "∃α' δ'.(set δ' ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ β @ [c] @ δ' @ [v] @ α' ∈ Tr⇘(induceES SES)⇙ 
      ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = [])"
    proof (cases)
      assume en: "En ρ s1 c"

      from c_in_C_inter_Y v_in_V_inter_Nabla s1_in_S s1''_in_S reachable_s1 s1_v_s1'' en fcrbe
      have "∃s1' ∈ S⇘SES⇙. ∃δ. (∀d ∈ (set δ). d ∈ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙))
        ∧ s1 ([c] @ δ @ [v]) ⟹⇘SES⇙ s1'
        ∧ (s1'', s1') ∈ ur"
        by (simp add: fcrbe_def)
      then  obtain s1' δ
        where s1'_in_S: "s1' ∈ S⇘SES⇙"
        and δ_in_N_inter_Delta_star: "(∀d ∈ (set δ). d ∈ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙))"
        and s1_cδv_s1': "s1 ([c] @ δ @ [v]) ⟹⇘SES⇙ s1'"
        and s1''_ur_s1': "(s1'', s1') ∈ ur"
        by (auto)

      have reachable_s1': "reachable SES s1'"
      proof -
        from s0_β_s1 s1_cδv_s1' have "s0⇘SES⇙ (β @ ([c] @ δ @ [v]))⟹⇘SES⇙ s1'"
          by (rule path_trans)
        thus ?thesis
          by (simp add: reachable_def, auto)
      qed
      
      from osc_property[OF osc s1'_in_S s1''_in_S α_contains_no_c reachable_s1' 
        reachable_s1'' enabled_s1''_α s1''_ur_s1']
      obtain α' 
        where  α'_contains_no_c: "α' ↿ C⇘𝒱⇙ = []"
        and α'_V_is_α_V: "α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙"
        and enabled_s1'_α': "enabled SES s1' α'" 
        by auto

      have βcδvα'_in_Tr: "β @ [c] @ δ @ [v] @ α' ∈ Tr⇘(induceES SES)⇙"
      proof -
        let ?l1 = "β @ [c] @ δ @ [v]"
        let ?l2 = "α'"
        from s0_β_s1 s1_cδv_s1' have "s0⇘SES⇙ (?l1)⟹⇘SES⇙ s1'"
          by (rule path_trans)
        moreover
        from enabled_s1'_α' obtain s1337 where "s1' ?l2⟹⇘SES⇙ s1337"
          by (simp add: enabled_def, auto)
        ultimately have "s0⇘SES⇙ (?l1 @ ?l2)⟹⇘SES⇙ s1337"
          by (rule path_trans)
        thus ?thesis
          by (simp add: induceES_def possible_traces_def enabled_def) 
      qed

      from δ_in_N_inter_Delta_star βcδvα'_in_Tr α'_V_is_α_V α'_contains_no_c
      show ?thesis
        by auto
    next
      assume not_en: "¬ En ρ s1 c"
      
      let ?A = "(Adm 𝒱 ρ Tr⇘(induceES SES)⇙ β c)"
      let ?E = "∃s ∈ S⇘SES⇙. (s0⇘SES⇙ β⟹⇘SES⇙ s ∧ En ρ s c)"

      { (* show the contraposition of Adm_to_En *)
        assume adm: "?A" 
        
        from s0_β_s1 have β_in_Tr: "β ∈ Tr⇘(induceES SES)⇙"
          by (simp add: induceES_def possible_traces_def enabled_def)
        
        from  β_in_Tr adm have "?E"
          by (rule Adm_to_En)
      }
      hence Adm_to_En_contr: "¬ ?E ⟹ ¬ ?A"
        by blast
      with s1_in_S s0_β_s1 not_en have not_adm: "¬ ?A"
        by auto
      with adm show ?thesis
        by auto
    qed  
  }
  thus ?thesis
    by (simp add: FCIA_def)
qed

theorem unwinding_theorem_SD:
"⟦ 𝒱' = ⦇ V = (V⇘𝒱⇙ ∪ N⇘𝒱⇙), N = {}, C = C⇘𝒱⇙ ⦈; 
  Unwinding.lrf SES 𝒱' ur; Unwinding.osc SES 𝒱' ur ⟧ 
  ⟹ SD 𝒱 Tr⇘(induceES SES)⇙"
proof -
  assume view'_def : "𝒱' = ⦇V = (V⇘𝒱⇙ ∪ N⇘𝒱⇙), N = {}, C = C⇘𝒱⇙⦈"
  assume lrf_view' : "Unwinding.lrf SES 𝒱' ur"
  assume osc_view' : "Unwinding.osc SES 𝒱' ur"

  interpret modified_view: Unwinding "SES" "𝒱'"
    by (unfold_locales, rule validSES, simp add: view'_def modified_view_valid)
      
  from lrf_view' osc_view' have BSD_view' : "BSD 𝒱' Tr⇘(induceES SES)⇙"
     by (rule_tac ur="ur" in modified_view.unwinding_theorem_BSD)
  with view'_def BSD_implies_SD_for_modified_view show ?thesis 
    by auto
qed

theorem unwinding_theorem_SI:
"⟦ 𝒱' = ⦇ V = (V⇘𝒱⇙ ∪ N⇘𝒱⇙), N = {}, C = C⇘𝒱⇙ ⦈; 
  Unwinding.lrb SES 𝒱' ur; Unwinding.osc SES 𝒱' ur ⟧ 
  ⟹ SI 𝒱 Tr⇘(induceES SES)⇙"
proof -
  assume view'_def : "𝒱' = ⦇V = V⇘𝒱⇙ ∪ N⇘𝒱⇙, N = {}, C = C⇘𝒱⇙⦈"
  assume lrb_view' : "Unwinding.lrb SES 𝒱' ur"
  assume osc_view' : "Unwinding.osc SES 𝒱' ur"

  interpret modified_view: Unwinding "SES" "𝒱'"
    by (unfold_locales, rule validSES, simp add: view'_def modified_view_valid)

  from lrb_view' osc_view' have BSI_view' : "BSI 𝒱' Tr⇘(induceES SES)⇙"
     by (rule_tac ur="ur" in modified_view.unwinding_theorem_BSI)
  with view'_def BSI_implies_SI_for_modified_view show ?thesis 
    by auto
qed

theorem unwinding_theorem_SIA: 
"⟦ 𝒱' = ⦇ V = (V⇘𝒱⇙ ∪ N⇘𝒱⇙), N = {}, C = C⇘𝒱⇙ ⦈; ρ 𝒱 = ρ 𝒱'; 
  Unwinding.lrbe SES 𝒱' ρ ur; Unwinding.osc SES 𝒱' ur ⟧ 
  ⟹ SIA ρ 𝒱 Tr⇘(induceES SES)⇙"
proof -
  assume view'_def : "𝒱' = ⦇V = V⇘𝒱⇙ ∪ N⇘𝒱⇙, N = {}, C = C⇘𝒱⇙⦈"
  assume ρ_eq : "ρ 𝒱 = ρ 𝒱'"
  assume lrbe_view' : "Unwinding.lrbe SES 𝒱' ρ ur"
  assume osc_view' : "Unwinding.osc SES 𝒱' ur"

  interpret modified_view: Unwinding "SES" "𝒱'"
    by (unfold_locales, rule validSES, simp add: view'_def modified_view_valid)

  from lrbe_view' osc_view' have BSIA_view' : "BSIA ρ 𝒱' Tr⇘(induceES SES)⇙"
     by (rule_tac ur="ur" in modified_view.unwinding_theorem_BSIA)
  with view'_def BSIA_implies_SIA_for_modified_view ρ_eq show ?thesis 
    by auto
qed 

theorem unwinding_theorem_SR:
"⟦ 𝒱' = ⦇ V = (V⇘𝒱⇙ ∪ N⇘𝒱⇙), N = {}, C = C⇘𝒱⇙ ⦈; 
  Unwinding.lrf SES 𝒱' ur; Unwinding.osc SES 𝒱' ur ⟧ 
  ⟹ SR 𝒱 Tr⇘(induceES SES)⇙"
proof -
  assume view'_def : "𝒱' = ⦇V = V⇘𝒱⇙ ∪ N⇘𝒱⇙, N = {}, C = C⇘𝒱⇙⦈"
  assume lrf_view' : "Unwinding.lrf SES 𝒱' ur"
  assume osc_view' : "Unwinding.osc SES 𝒱' ur"

  from lrf_view' osc_view' view'_def have S_view : "SD 𝒱 Tr⇘(induceES SES)⇙"
     by (rule_tac ur="ur" in  unwinding_theorem_SD, auto)
  with SD_implies_SR show ?thesis
    by auto
qed

theorem unwinding_theorem_D:
"⟦ lrf ur; osc ur ⟧ ⟹ D 𝒱 Tr⇘(induceES SES)⇙"
proof -
  assume "lrf ur"
  and "osc ur"
  hence "BSD 𝒱 Tr⇘(induceES SES)⇙"
    by (rule unwinding_theorem_BSD)
  thus ?thesis
    by (rule BSD_implies_D)
qed

theorem unwinding_theorem_I:
"⟦ lrb ur; osc ur ⟧ ⟹ I 𝒱 Tr⇘(induceES SES)⇙"
proof -
  assume "lrb ur"
  and "osc ur"
  hence "BSI 𝒱 Tr⇘(induceES SES)⇙"
    by (rule unwinding_theorem_BSI)
  thus ?thesis
    by (rule BSI_implies_I)
qed

theorem unwinding_theorem_IA:
"⟦ lrbe ρ ur; osc ur ⟧ ⟹ IA ρ 𝒱 Tr⇘(induceES SES)⇙"
proof -
  assume "lrbe ρ ur"
  and "osc ur"
  hence "BSIA ρ 𝒱 Tr⇘(induceES SES)⇙"
    by (rule unwinding_theorem_BSIA)
  thus ?thesis
    by (rule BSIA_implies_IA)
qed

theorem unwinding_theorem_R:
"⟦ lrf ur; osc ur ⟧ ⟹ R 𝒱 (Tr⇘(induceES SES)⇙)"
proof -
  assume "lrf ur"
  and "osc ur"
  hence "BSD 𝒱 Tr⇘(induceES SES)⇙"
    by (rule unwinding_theorem_BSD)
  hence "D 𝒱 Tr⇘(induceES SES)⇙"
    by (rule BSD_implies_D)
  thus ?thesis
    by (rule D_implies_R)
qed

end

end