Theory Timed_Automata.Closure

theory Closure
  imports Regions
begin

section ‹Correct Approximation of Zones with ‹α›-regions›

locale AlphaClosure =
  fixes X k ℛ and V :: "('c, t) cval set"
  defines "ℛ ≡ {region X I r | I r. valid_region X k I r}"
  defines "V ≡ {v . ∀ x ∈ X. v x ≥ 0}"
  assumes finite: "finite X"
begin

lemmas set_of_regions_spec = set_of_regions[OF _ _ _ finite, of _ k, folded ℛ_def]
lemmas region_cover_spec = region_cover[of X _ k, folded ℛ_def]
lemmas region_unique_spec = region_unique[of ℛ X k, folded ℛ_def, simplified]
lemmas regions_closed'_spec = regions_closed'[of ℛ X k, folded ℛ_def, simplified]

lemma valid_regions_distinct_spec:
  "R ∈ ℛ ⟹ R' ∈ ℛ ⟹ v ∈ R ⟹ v ∈ R' ⟹ R = R'"
unfolding ℛ_def using valid_regions_distinct
by auto (drule valid_regions_distinct, assumption+, simp)+

definition cla ("Closure⇩α _" [71] 71)
where
  "cla Z = ⋃ {R ∈ ℛ. R ∩ Z ≠ {}}"


subsubsection ‹The nice and easy properties proved by Bouyer›

lemma closure_constraint_id:
  "∀(x, m)∈collect_clock_pairs g. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ ⟹ Closure⇩α ⦃g⦄ = ⦃g⦄ ∩ V"
proof goal_cases
  case 1
  show ?case
  proof auto
    fix v assume v: "v ∈ Closure⇩α ⦃g⦄"
    then obtain R where R: "v ∈ R" "R ∈ ℛ" "R ∩ ⦃g⦄ ≠ {}" unfolding cla_def by auto
    with ccompatible[OF 1, folded ℛ_def] show "v ∈ ⦃g⦄" unfolding ccompatible_def by auto
    from R show "v ∈ V" unfolding V_def ℛ_def by auto
  next
    fix v assume v: "v ∈ ⦃g⦄" "v ∈ V"
    with region_cover[of X v k, folded ℛ_def] obtain R where "R ∈ ℛ" "v ∈ R" unfolding V_def by auto
    then show "v ∈ Closure⇩α ⦃g⦄" unfolding cla_def using v by auto
  qed
qed

lemma closure_id':
  "Z ≠ {} ⟹ Z ⊆ R ⟹ R ∈ ℛ ⟹ Closure⇩α Z = R"
proof goal_cases
  case 1
  note A = this
  then have "R ⊆ Closure⇩α Z" unfolding cla_def by auto
  moreover
  { fix R' assume R': "Z ∩ R' ≠ {}" "R' ∈ ℛ" "R ≠ R'"
    with A obtain v where "v ∈ R" "v ∈ R'" by auto
    with ℛ_regions_distinct[OF _ A(3) this(1) R'(2-)] ℛ_def have False by auto
  }
  ultimately show ?thesis unfolding cla_def by auto
qed

lemma closure_id:
  "Closure⇩α Z ≠ {} ⟹ Z ⊆ R ⟹ R ∈ ℛ ⟹ Closure⇩α Z = R"
proof goal_cases
  case 1
  then have "Z ≠ {}" unfolding cla_def by auto
  with 1 closure_id' show ?case by blast
qed

lemma closure_update_mono:
  "Z ⊆ V ⟹ set r ⊆ X ⟹ zone_set (Closure⇩α Z) r ⊆ Closure⇩α(zone_set Z r)"
proof -
  assume A: "Z ⊆ V" "set r ⊆ X"
  let ?U = "{R ∈ ℛ. Z ∩ R ≠ {}}"
  from A(1) region_cover_spec  have "∀ v ∈ Z. ∃ R. R ∈ ℛ ∧ v ∈ R" unfolding V_def by auto
  then have "Z = ⋃ {Z ∩ R | R. R ∈ ?U}"
  proof (auto, goal_cases)
    case (1 v)
    then obtain R where "R ∈ ℛ" "v ∈ R" by auto
    moreover with 1 have "Z ∩ R ≠ {}" "v ∈ Z ∩ R" by auto
    ultimately show ?case by auto
  qed
  then obtain U where U: "Z = ⋃ {Z ∩ R | R. R ∈ U}" "∀ R ∈ U. R ∈ ℛ" by blast
  { fix R assume R: "R ∈ U"
    { fix v' assume v': "v' ∈ zone_set (Closure⇩α (Z ∩ R)) r - Closure⇩α(zone_set (Z ∩ R) r)"
      then obtain v where *:
        "v ∈ Closure⇩α (Z ∩ R)" "v' = [r → 0]v"
      unfolding zone_set_def by auto
      with closure_id[of "Z ∩ R" R] R U(2) have **:
        "Closure⇩α (Z ∩ R) = R" "Closure⇩α (Z ∩ R) ∈ ℛ"
      by fastforce+
      with region_set'_id[OF _ *(1) finite _ _ A(2), of k 0, folded ℛ_def, OF this(2)]
      have ***: "zone_set R r ∈ ℛ" "[r→0]v ∈ zone_set R r"
      unfolding zone_set_def region_set'_def by auto
      from * have "Z ∩ R ≠ {}" unfolding cla_def by auto
      then have "zone_set (Z ∩ R) r ≠ {}" unfolding zone_set_def by auto
      from closure_id'[OF this _ ***(1)] have "Closure⇩α zone_set (Z ∩ R) r = zone_set R r"
      unfolding zone_set_def by auto
      with v' **(1) have False by auto
    }
    then have "zone_set (Closure⇩α (Z ∩ R)) r ⊆ Closure⇩α(zone_set (Z ∩ R) r)" by auto
  } note Z_i = this
  from U(1) have "Closure⇩α Z = ⋃ {Closure⇩α (Z ∩ R) | R. R ∈ U}" unfolding cla_def by auto
  then have "zone_set (Closure⇩α Z) r = ⋃ {zone_set (Closure⇩α (Z ∩ R)) r | R. R ∈ U}"
  unfolding zone_set_def by auto
  also have "… ⊆ ⋃ {Closure⇩α(zone_set (Z ∩ R) r) | R. R ∈ U}" using Z_i by auto
  also have "… = Closure⇩α ⋃ {(zone_set (Z ∩ R) r) | R. R ∈ U}" unfolding cla_def by auto
  also have "… = Closure⇩α zone_set (⋃ {Z ∩ R| R. R ∈ U}) r"
  proof goal_cases
    case 1
    have "zone_set (⋃ {Z ∩ R| R. R ∈ U}) r = ⋃ {(zone_set (Z ∩ R) r) | R. R ∈ U}"
    unfolding zone_set_def by auto
    then show ?case by auto
  qed
  finally show "zone_set (Closure⇩α Z) r ⊆ Closure⇩α(zone_set Z r)" using U by simp
qed

lemma SuccI3:
  "R ∈ ℛ ⟹ v ∈ R ⟹ t ≥ 0 ⟹ (v ⊕ t) ∈ R' ⟹ R' ∈ ℛ ⟹ R' ∈ Succ ℛ R"
 apply (intro SuccI2[of ℛ X k, folded ℛ_def, simplified])
    apply assumption+
   apply (intro region_unique[of ℛ X k, folded ℛ_def, simplified, symmetric])
by assumption+

lemma closure_delay_mono:
  "Z ⊆ V ⟹ (Closure⇩α Z)⇧↑ ⊆ Closure⇩α (Z⇧↑)"
proof
  fix v assume v: "v ∈ (Closure⇩α Z)⇧↑" and Z: "Z ⊆ V"
  then obtain u u' t R where A:
    "u ∈ Closure⇩α Z" "v = (u ⊕ t)" "u ∈ R" "u' ∈ R" "R ∈ ℛ" "u' ∈ Z" "t ≥ 0"
  unfolding cla_def zone_delay_def by blast
  from A(3,5) have "∀ x ∈ X. u x ≥ 0" unfolding ℛ_def by fastforce
  with region_cover_spec[of v] A(2,7) obtain R' where R':
    "R' ∈ ℛ" "v ∈ R'"
  unfolding cval_add_def by auto
  with set_of_regions_spec[OF A(5,4), OF SuccI3, of u] A obtain t where t:
    "t ≥ 0" "[u' ⊕ t]⇩ℛ = R'"
  by auto
  with A have "(u' ⊕ t) ∈ Z⇧↑" unfolding zone_delay_def by auto
  moreover from regions_closed'_spec[OF A(5,4)] t have "(u' ⊕ t) ∈ R'" by auto
  ultimately have "R' ∩ (Z⇧↑) ≠ {}" by auto
  with R' show "v ∈ Closure⇩α (Z⇧↑)" unfolding cla_def by auto
qed

lemma region_V: "R ∈ ℛ ⟹ R ⊆ V" using V_def ℛ_def region.cases by auto

lemma closure_V:
  "Closure⇩α Z ⊆ V"
unfolding cla_def using region_V by auto

lemma closure_V_int:
  "Closure⇩α Z = Closure⇩α (Z ∩ V)"
unfolding cla_def using region_V by auto

lemma closure_constraint_mono:
  "Closure⇩α g = g ⟹ g ∩ (Closure⇩α Z) ⊆ Closure⇩α (g ∩ Z)"
unfolding cla_def by auto

lemma closure_constraint_mono':
  assumes "Closure⇩α g = g ∩ V"
  shows "g ∩ (Closure⇩α Z) ⊆ Closure⇩α (g ∩ Z)"
proof -
  from assms closure_V_int have "Closure⇩α (g ∩ V) = g ∩ V" by auto
  from closure_constraint_mono[OF this, of Z] have
    "g ∩ (V ∩ Closure⇩α Z) ⊆ Closure⇩α (g ∩ Z ∩ V)"
  by (metis Int_assoc Int_commute)
  with closure_V[of Z] closure_V_int[of "g ∩ Z"] show ?thesis by auto
qed

lemma cla_empty_iff:
  "Z ⊆ V ⟹ Z = {} ⟷ Closure⇩α Z = {}"
unfolding cla_def V_def using region_cover_spec by fast

lemma closure_involutive_aux:
  "U ⊆ ℛ ⟹ Closure⇩α ⋃ U = ⋃ U"
unfolding cla_def using valid_regions_distinct_spec by blast

lemma closure_involutive_aux':
  "∃ U. U ⊆ ℛ ∧ Closure⇩α Z = ⋃ U"
unfolding cla_def by (rule exI[where x = "{R ∈ ℛ. R ∩ Z ≠ {}}"]) auto

lemma closure_involutive:
  "Closure⇩α Closure⇩α Z = Closure⇩α Z"
using closure_involutive_aux closure_involutive_aux' by metis

lemma closure_involutive':
  "Z ⊆ Closure⇩α W ⟹ Closure⇩α Z ⊆ Closure⇩α W"
unfolding cla_def using valid_regions_distinct_spec by fast

lemma closure_subs:
  "Z ⊆ V ⟹ Z ⊆ Closure⇩α Z"
unfolding cla_def V_def using region_cover_spec by fast

lemma cla_mono':
  "Z' ⊆ V ⟹ Z ⊆ Z' ⟹ Closure⇩α Z ⊆ Closure⇩α Z'"
by (meson closure_involutive' closure_subs subset_trans)

lemma cla_mono:
  "Z ⊆ Z' ⟹ Closure⇩α Z ⊆ Closure⇩α Z'"
using closure_V_int cla_mono'[of "Z' ∩ V" "Z ∩ V"] by auto


section ‹A New Zone Semantics Abstracting with ‹Closure⇩α››

subsection ‹Single step›

inductive step_z_alpha ::
  "('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 's ⇒ ('c, t) zone ⇒ bool"
("_ ⊢ ⟨_, _⟩ ↝⇩α ⟨_, _⟩" [61,61,61] 61)
where
  step_alpha: "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l', Closure⇩α Z'⟩"

inductive_cases[elim!]: "A ⊢ ⟨l, u⟩ ↝⇩α ⟨l',u'⟩"

declare step_z_alpha.intros[intro]

lemma up_V: "Z ⊆ V ⟹ Z⇧↑ ⊆ V"
unfolding V_def zone_delay_def cval_add_def by auto

lemma reset_V: "Z ⊆ V ⟹ (zone_set Z r) ⊆ V"
unfolding V_def unfolding zone_set_def by (induction r, auto)

lemma step_z_V: "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ⊆ V"
 apply (induction rule: step_z.induct)
  apply (rule le_infI1)
  apply (rule up_V)
  apply blast
 apply (rule le_infI1)
 apply (rule reset_V)
by blast


text ‹Single-step soundness and completeness follows trivially from ‹cla_empty_iff›.›

lemma step_z_alpha_sound:
  "A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z''⟩ ∧ Z'' ≠ {}"
 apply (induction rule: step_z_alpha.induct)
  apply (frule step_z_V)
  apply assumption
 apply (rotate_tac 3)
 apply (drule cla_empty_iff)
by auto

lemma step_z_alpha_complete:
  "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l',Z''⟩ ∧ Z'' ≠ {}"
 apply (frule step_z_V)
  apply assumption
 apply (rotate_tac 3)
 apply (drule cla_empty_iff)
by auto

lemma zone_set_mono:
  "A ⊆ B ⟹ zone_set A r ⊆ zone_set B r"
unfolding zone_set_def by auto

lemma zone_delay_mono:
  "A ⊆ B ⟹ A⇧↑ ⊆ B⇧↑"
unfolding zone_delay_def by auto


subsection ‹Multi step›

inductive
  steps_z_alpha :: "('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 's ⇒ ('c, t) zone ⇒ bool"
("_ ⊢ ⟨_, _⟩ ↝⇩α* ⟨_, _⟩" [61,61,61] 61)
where
  refl: "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l, Z⟩" |
  step: "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l', Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝⇩α ⟨l'', Z''⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l'', Z''⟩"

declare steps_z_alpha.intros[intro]

lemma subset_int_mono: "A ⊆ B ⟹ A ∩ C ⊆ B ∩ C" by blast

text ‹P. Bouyer's calculation for @{term "Post(Closure⇩α Z, e) ⊆ Closure⇩α(Post (Z, e))"}›
text ‹This is now obsolete as we argue solely with monotonicty of ‹steps_z› w.r.t ‹Closure⇩α››

lemma calc:
  "valid_abstraction A X k ⟹ Z ⊆ V ⟹ A ⊢ ⟨l, Closure⇩α Z⟩ ↝ ⟨l', Z'⟩
  ⟹ ∃Z''. A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l', Z''⟩ ∧ Z' ⊆ Z''"
proof (cases rule: step_z.cases, assumption, goal_cases)
  case 1
  note A = this
  from A(1) have "∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
  by (fastforce elim: valid_abstraction.cases)
  then have "∀(x, m)∈collect_clock_pairs (inv_of A l). m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
  unfolding clkp_set_def collect_clki_def inv_of_def by auto
  from closure_constraint_id[OF this] have *: "Closure⇩α ⦃inv_of A l⦄ = ⦃inv_of A l⦄ ∩ V" .
  from closure_constraint_mono'[OF *, of Z] have
    "(Closure⇩α Z) ∩ {u. u ⊢ inv_of A l} ⊆ Closure⇩α (Z ∩ {u. u ⊢ inv_of A l})"
  unfolding ccval_def by (subst Int_commute) (subst (asm) (2) Int_commute, assumption)
  moreover have "…⇧↑ ⊆ Closure⇩α ((Z ∩ {u. u ⊢ inv_of A l})⇧↑)" using A(2) by (blast intro!: closure_delay_mono)
  ultimately have "Z' ⊆ Closure⇩α ((Z ∩ {u. u ⊢ inv_of A l})⇧↑ ∩ {u. u ⊢ inv_of A l})"
  using closure_constraint_mono'[OF *, of "(Z ∩ {u. u ⊢ inv_of A l})⇧↑"] unfolding ccval_def
   apply (subst A(5))
   apply (subst (asm) (5 7) Int_commute)
   apply (rule subset_trans)
    defer
    apply assumption
   apply (subst subset_int_mono)
    defer
    apply rule
   apply (rule subset_trans)
    defer
    apply assumption
   apply (rule zone_delay_mono)
   apply assumption
  done
  with A(4,3) show ?thesis by auto
next
  case (2 g a r)
  note A = this
  from A(1) have *:
    "∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
    "collect_clkvt (trans_of A) ⊆ X"
    "finite X"
  by (auto elim: valid_abstraction.cases)
  from *(1) A(5) have "∀(x, m)∈collect_clock_pairs (inv_of A l'). m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
  unfolding clkp_set_def collect_clki_def inv_of_def by fastforce
  from closure_constraint_id[OF this] have **: "Closure⇩α ⦃inv_of A l'⦄ = ⦃inv_of A l'⦄ ∩ V" .
  from *(1) A(5) have "∀(x, m)∈collect_clock_pairs g. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
  unfolding clkp_set_def collect_clkt_def by fastforce
  from closure_constraint_id[OF this] have ***: "Closure⇩α ⦃g⦄ = ⦃g⦄ ∩ V" .
  from *(2) A(5) have ****: "set r ⊆ X" unfolding collect_clkvt_def by fastforce
  from closure_constraint_mono'[OF ***, of Z] have
    "(Closure⇩α Z) ∩ {u. u ⊢ g} ⊆ Closure⇩α (Z ∩ {u. u ⊢ g})" unfolding ccval_def
  by (subst Int_commute) (subst (asm) (2) Int_commute, assumption)
  moreover have "zone_set … r ⊆ Closure⇩α (zone_set (Z ∩ {u. u ⊢ g}) r)" using **** A(2)
  by (intro closure_update_mono, auto)
  ultimately have "Z' ⊆ Closure⇩α (zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'})"
  using closure_constraint_mono'[OF **, of "zone_set (Z ∩ {u. u ⊢ g}) r"] unfolding ccval_def
    apply (subst A(4))
    apply (subst (asm) (5 7) Int_commute)
    apply (rule subset_trans)
     defer
     apply assumption
    apply (subst subset_int_mono)
     defer
     apply rule
    apply (rule subset_trans)
     defer
     apply assumption
    apply (rule zone_set_mono)
    apply assumption
  done
  with A(5) show ?thesis by auto
qed


text ‹
  Turning P. Bouyers argument for multiple steps into an inductive proof is not direct.
  With this initial argument we can get to a point where the induction hypothesis is applicable.
  This breaks the "information hiding" induced by the different variants of steps.
›

lemma steps_z_alpha_closure_involutive'_aux:
  "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ Closure⇩α Z ⊆ Closure⇩α W ⟹ valid_abstraction A X k ⟹ Z ⊆ V
  ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝ ⟨l',W'⟩ ∧ Closure⇩α Z' ⊆ Closure⇩α W'"
proof (induction rule: step_z.induct)
  case A: (step_t_z A l Z)
  let ?Z' = "(Z ∩ {u. u ⊢ inv_of A l})⇧↑ ∩ {u. u ⊢ inv_of A l}"
  let ?W' = "(W ∩ {u. u ⊢ inv_of A l})⇧↑ ∩ {u. u ⊢ inv_of A l}"
  from ℛ_def have ℛ_def': "ℛ = {region X I r |I r. valid_region X k I r}" by simp
  have step_z: "A ⊢ ⟨l, W⟩ ↝ ⟨l,?W'⟩" by auto
  moreover have "Closure⇩α ?Z' ⊆ Closure⇩α ?W'"
  proof
    fix v assume v: "v ∈ Closure⇩α ?Z'"
    then obtain R' v' where 1: "R' ∈ ℛ" "v ∈ R'" "v' ∈ R'" "v' ∈ ?Z'" unfolding cla_def by auto
    then obtain u d where
      "u ∈ Z" and v': "v' = u ⊕ d" "u ⊢ inv_of A l" "u ⊕ d ⊢ inv_of A l" "0 ≤ d"
    unfolding zone_delay_def by blast
    with closure_subs[OF A(3)] A(1) obtain u' R where u': "u' ∈ W" "u ∈ R" "u' ∈ R" "R ∈ ℛ"
    unfolding cla_def by blast
    then have "∀x∈X. 0 ≤ u x" unfolding ℛ_def by fastforce
    from region_cover'[OF ℛ_def' this] have R: "[u]⇩ℛ ∈ ℛ" "u ∈ [u]⇩ℛ" by auto
    from SuccI2[OF ℛ_def' this(2,1) v'(4), of "[v']⇩ℛ"] v'(1) have v'1:
      "[v']⇩ℛ ∈ Succ ℛ ([u]⇩ℛ)" "[v']⇩ℛ ∈ ℛ"
    by auto
    from regions_closed'_spec[OF R(1,2) v'(4)] v'(1) have v'2: "v' ∈ [v']⇩ℛ" by simp
    from A(2) have *:
      "∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
      "collect_clkvt (trans_of A) ⊆ X"
      "finite X"
    by (auto elim: valid_abstraction.cases)
    from *(1) u'(2) have "∀(x, m)∈collect_clock_pairs (inv_of A l). m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
    unfolding clkp_set_def collect_clki_def inv_of_def by fastforce
    from ccompatible[OF this, folded ℛ_def'] v'1(2) v'2 v'(1,2,3) R have 3:
      "[v']⇩ℛ ⊆ ⦃inv_of A l⦄" "([u]⇩ℛ) ⊆ ⦃inv_of A l⦄"
    unfolding ccompatible_def ccval_def by auto
    with A v'1 R(1) ℛ_def' have "A,ℛ ⊢ ⟨l, ([u]⇩ℛ)⟩ ↝ ⟨l,([v']⇩ℛ)⟩" by auto
    with valid_regions_distinct_spec[OF v'1(2) 1(1) v'2 1(3)] region_unique_spec[OF u'(2,4)]
    have step_r: "A,ℛ ⊢ ⟨l, R⟩ ↝ ⟨l, R'⟩" and 2: "[v']⇩ℛ = R'" "[u]⇩ℛ = R" by auto
    from set_of_regions_spec[OF u'(4,3)] v'1(1) 2 obtain t where t: "t ≥ 0" "[u' ⊕ t]⇩ℛ = R'" by auto
    with regions_closed'_spec[OF u'(4,3) this(1)] step_t_r(1) have *: "u' ⊕ t ∈ R'" by auto
    with t(1) 3 2 u'(1,3) have "A ⊢ ⟨l, u'⟩ → ⟨l, u' ⊕ t⟩" "u' ⊕ t ∈ ?W'"
    unfolding zone_delay_def ccval_def by auto
    with * 1(1) have "R' ⊆ Closure⇩α ?W'" unfolding cla_def by auto
    with 1(2) show "v ∈ Closure⇩α ?W'" ..
  qed
  ultimately show ?case by auto
next
  case A: (step_a_z A l g a r l' Z)
  let ?Z' = "zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
  let ?W' = "zone_set (W ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
  from ℛ_def have ℛ_def': "ℛ = {region X I r |I r. valid_region X k I r}" by simp
  from A(1) have step_z: "A ⊢ ⟨l, W⟩ ↝ ⟨l',?W'⟩" by auto
  moreover have "Closure⇩α ?Z' ⊆ Closure⇩α ?W'"
  proof
    fix v assume v: "v ∈ Closure⇩α ?Z'"
    then obtain R' v' where 1: "R' ∈ ℛ" "v ∈ R'" "v' ∈ R'" "v' ∈ ?Z'" unfolding cla_def by auto
    then obtain u where
      "u ∈ Z" and v': "v' = [r→0]u" "u ⊢ g" "v' ⊢ inv_of A l'"
    unfolding zone_set_def by blast
    let ?R'= "region_set' (([u]⇩ℛ) ∩ {u. u ⊢ g}) r 0 ∩ {u. u ⊢ inv_of A l'}"
    from ‹u ∈ Z› closure_subs[OF A(4)] A(2) obtain u' R where u': "u' ∈ W" "u ∈ R" "u' ∈ R" "R ∈ ℛ"
    unfolding cla_def by blast
    then have "∀x∈X. 0 ≤ u x" unfolding ℛ_def by fastforce
    from region_cover'[OF ℛ_def' this] have R: "[u]⇩ℛ ∈ ℛ" "u ∈ [u]⇩ℛ" by auto
    from step_r_complete_aux[OF ℛ_def' A(3) this(2,1) A(1) v'(2)] v'
    have *: "[u]⇩ℛ = ([u]⇩ℛ) ∩ {u. u ⊢ g}" "?R' = region_set' ([u]⇩ℛ) r 0" "?R' ∈ ℛ" by auto
    from ℛ_def' A(3) have "collect_clkvt (trans_of A) ⊆ X" "finite X"
    by (auto elim: valid_abstraction.cases)
    with A(1) have r: "set r ⊆ X" unfolding collect_clkvt_def by fastforce
    from * v'(1) R(2) have "v' ∈ ?R'" unfolding region_set'_def by auto
    moreover have "A,ℛ ⊢ ⟨l,([u]⇩ℛ)⟩ ↝ ⟨l',?R'⟩" using R(1) ℛ_def' A(1,3) v'(2) by auto
    thm valid_regions_distinct_spec
    with valid_regions_distinct_spec[OF *(3) 1(1) ‹v' ∈ ?R'› 1(3)] region_unique_spec[OF u'(2,4)]
    have 2: "?R' = R'" "[u]⇩ℛ = R" by auto
    with * u' have *: "[r→0]u' ∈ ?R'" "u' ⊢ g" "[r→0]u' ⊢ inv_of A l'"
    unfolding region_set'_def by auto
    with A(1) have "A ⊢ ⟨l, u'⟩ → ⟨l',[r→0]u'⟩" apply (intro step.intros(1)) apply rule by auto
    moreover from * u'(1) have "[r→0]u' ∈ ?W'" unfolding zone_set_def by auto
    ultimately have "R' ⊆ Closure⇩α ?W'" using *(1) 1(1) 2(1) unfolding cla_def by auto
    with 1(2) show "v ∈ Closure⇩α ?W'" ..
  qed
  ultimately show ?case by meson
qed

lemma steps_z_alpha_closure_involutive'_aux':
  "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ Closure⇩α Z ⊆ Closure⇩α W ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ W ⊆ Z
  ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝ ⟨l',W'⟩ ∧ Closure⇩α Z' ⊆ Closure⇩α W' ∧ W' ⊆ Z'"
proof (induction rule: step_z.induct)
  case A: (step_t_z A l Z)
  let ?Z' = "(Z ∩ {u. u ⊢ inv_of A l})⇧↑ ∩ {u. u ⊢ inv_of A l}"
  let ?W' = "(W ∩ {u. u ⊢ inv_of A l})⇧↑ ∩ {u. u ⊢ inv_of A l}"
  from ℛ_def have ℛ_def': "ℛ = {region X I r |I r. valid_region X k I r}" by simp
  have step_z: "A ⊢ ⟨l, W⟩ ↝ ⟨l,?W'⟩" by auto
  moreover have "Closure⇩α ?Z' ⊆ Closure⇩α ?W'"
  proof
    fix v assume v: "v ∈ Closure⇩α ?Z'"
    then obtain R' v' where 1: "R' ∈ ℛ" "v ∈ R'" "v' ∈ R'" "v' ∈ ?Z'" unfolding cla_def by auto
    then obtain u d where
      "u ∈ Z" and v': "v' = u ⊕ d" "u ⊢ inv_of A l" "u ⊕ d ⊢ inv_of A l" "0 ≤ d"
    unfolding zone_delay_def by blast
    with closure_subs[OF A(3)] A(1) obtain u' R where u': "u' ∈ W" "u ∈ R" "u' ∈ R" "R ∈ ℛ"
    unfolding cla_def by blast
    then have "∀x∈X. 0 ≤ u x" unfolding ℛ_def by fastforce
    from region_cover'[OF ℛ_def' this] have R: "[u]⇩ℛ ∈ ℛ" "u ∈ [u]⇩ℛ" by auto
    from SuccI2[OF ℛ_def' this(2,1) v'(4), of "[v']⇩ℛ"] v'(1) have v'1:
      "[v']⇩ℛ ∈ Succ ℛ ([u]⇩ℛ)" "[v']⇩ℛ ∈ ℛ"
    by auto
    from regions_closed'_spec[OF R(1,2) v'(4)] v'(1) have v'2: "v' ∈ [v']⇩ℛ" by simp
    from A(2) have *:
      "∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
      "collect_clkvt (trans_of A) ⊆ X"
      "finite X"
    by (auto elim: valid_abstraction.cases)
    from *(1) u'(2) have "∀(x, m)∈collect_clock_pairs (inv_of A l). m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
    unfolding clkp_set_def collect_clki_def inv_of_def by fastforce
    from ccompatible[OF this, folded ℛ_def'] v'1(2) v'2 v'(1,2,3) R have 3:
      "[v']⇩ℛ ⊆ ⦃inv_of A l⦄" "([u]⇩ℛ) ⊆ ⦃inv_of A l⦄"
    unfolding ccompatible_def ccval_def by auto
    with A v'1 R(1) ℛ_def' have "A,ℛ ⊢ ⟨l, ([u]⇩ℛ)⟩ ↝ ⟨l,([v']⇩ℛ)⟩" by auto
    with valid_regions_distinct_spec[OF v'1(2) 1(1) v'2 1(3)] region_unique_spec[OF u'(2,4)]
    have step_r: "A,ℛ ⊢ ⟨l, R⟩ ↝ ⟨l, R'⟩" and 2: "[v']⇩ℛ = R'" "[u]⇩ℛ = R" by auto
    from set_of_regions_spec[OF u'(4,3)] v'1(1) 2 obtain t where t: "t ≥ 0" "[u' ⊕ t]⇩ℛ = R'" by auto
    with regions_closed'_spec[OF u'(4,3) this(1)] step_t_r(1) have *: "u' ⊕ t ∈ R'" by auto
    with t(1) 3 2 u'(1,3) have "A ⊢ ⟨l, u'⟩ → ⟨l, u' ⊕ t⟩" "u' ⊕ t ∈ ?W'"
    unfolding zone_delay_def ccval_def by auto
    with * 1(1) have "R' ⊆ Closure⇩α ?W'" unfolding cla_def by auto
    with 1(2) show "v ∈ Closure⇩α ?W'" ..
  qed
  moreover have "?W' ⊆ ?Z'" using ‹W ⊆ Z› unfolding zone_delay_def by auto
  ultimately show ?case by auto
next
  case A: (step_a_z A l g a r l' Z)
  let ?Z' = "zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
  let ?W' = "zone_set (W ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
  from ℛ_def have ℛ_def': "ℛ = {region X I r |I r. valid_region X k I r}" by simp
  from A(1) have step_z: "A ⊢ ⟨l, W⟩ ↝ ⟨l',?W'⟩" by auto
  moreover have "Closure⇩α ?Z' ⊆ Closure⇩α ?W'"
  proof
    fix v assume v: "v ∈ Closure⇩α ?Z'"
    then obtain R' v' where 1: "R' ∈ ℛ" "v ∈ R'" "v' ∈ R'" "v' ∈ ?Z'" unfolding cla_def by auto
    then obtain u where
      "u ∈ Z" and v': "v' = [r→0]u" "u ⊢ g" "v' ⊢ inv_of A l'"
    unfolding zone_set_def by blast
    let ?R'= "region_set' (([u]⇩ℛ) ∩ {u. u ⊢ g}) r 0 ∩ {u. u ⊢ inv_of A l'}"
    from ‹u ∈ Z› closure_subs[OF A(4)] A(2) obtain u' R where u': "u' ∈ W" "u ∈ R" "u' ∈ R" "R ∈ ℛ"
    unfolding cla_def by blast
    then have "∀x∈X. 0 ≤ u x" unfolding ℛ_def by fastforce
    from region_cover'[OF ℛ_def' this] have R: "[u]⇩ℛ ∈ ℛ" "u ∈ [u]⇩ℛ" by auto
    from step_r_complete_aux[OF ℛ_def' A(3) this(2,1) A(1) v'(2)] v'
    have *: "[u]⇩ℛ = ([u]⇩ℛ) ∩ {u. u ⊢ g}" "?R' = region_set' ([u]⇩ℛ) r 0" "?R' ∈ ℛ" by auto
    from ℛ_def' A(3) have "collect_clkvt (trans_of A) ⊆ X" "finite X"
    by (auto elim: valid_abstraction.cases)
    with A(1) have r: "set r ⊆ X" unfolding collect_clkvt_def by fastforce
    from * v'(1) R(2) have "v' ∈ ?R'" unfolding region_set'_def by auto
    moreover have "A,ℛ ⊢ ⟨l,([u]⇩ℛ)⟩ ↝ ⟨l',?R'⟩" using R(1) ℛ_def' A(1,3) v'(2) by auto
    thm valid_regions_distinct_spec
    with valid_regions_distinct_spec[OF *(3) 1(1) ‹v' ∈ ?R'› 1(3)] region_unique_spec[OF u'(2,4)]
    have 2: "?R' = R'" "[u]⇩ℛ = R" by auto
    with * u' have *: "[r→0]u' ∈ ?R'" "u' ⊢ g" "[r→0]u' ⊢ inv_of A l'"
    unfolding region_set'_def by auto
    with A(1) have "A ⊢ ⟨l, u'⟩ → ⟨l',[r→0]u'⟩" apply (intro step.intros(1)) apply rule by auto
    moreover from * u'(1) have "[r→0]u' ∈ ?W'" unfolding zone_set_def by auto
    ultimately have "R' ⊆ Closure⇩α ?W'" using *(1) 1(1) 2(1) unfolding cla_def by auto
    with 1(2) show "v ∈ Closure⇩α ?W'" ..
  qed
  moreover have "?W' ⊆ ?Z'" using ‹W ⊆ Z› unfolding zone_set_def by auto
  ultimately show ?case by meson
qed

lemma steps_z_alt:
  "A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',Z''⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z''⟩"
by (induction rule: steps_z.induct) auto

lemma steps_z_alpha_V: "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ⊆ V"
apply (induction rule: steps_z_alpha.induct) using closure_V by auto

lemma steps_z_alpha_closure_involutive':
  "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',Z''⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V
  ⟹ ∃ Z'''. A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z'''⟩ ∧ Closure⇩α Z'' ⊆ Closure⇩α Z''' ∧ Z''' ⊆ Z''"
proof (induction A l Z l' Z' arbitrary: Z'' l'' rule: steps_z_alpha.induct, goal_cases)
  case refl from this(1) show ?case by blast
next
  case A: (2 A l Z l' Z' l'' Z'' Z''a l''a)
  from A(3) obtain 𝒵 where Z'': "Z'' = Closure⇩α 𝒵" "A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',𝒵⟩" by auto
  from A(2)[OF Z''(2) A(5,6)] obtain Z''' where Z''':
    "A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z'''⟩" "Closure⇩α 𝒵 ⊆ Closure⇩α Z'''" "Z''' ⊆ 𝒵"
  by auto
  from closure_subs have *:
    "Z''' ⊆ Closure⇩α 𝒵"
  by (metis A(1,6) Z'''(3) Z''(2) step_z_V steps_z_alpha_V subset_trans) 
  from A(4) Z'' have "A ⊢ ⟨l'', Closure⇩α 𝒵⟩ ↝ ⟨l''a,Z''a⟩" by auto
  from steps_z_alpha_closure_involutive'_aux'[OF this(1) _ A(5) closure_V *] Z'''(2,3) obtain W'
    where ***: "A ⊢ ⟨l'', Z'''⟩ ↝ ⟨l''a,W'⟩" "Closure⇩α Z''a ⊆ Closure⇩α W'" "W' ⊆ Z''a"
  by (auto simp: closure_involutive)
  with Z'''(1) have "A ⊢ ⟨l, Z⟩ ↝* ⟨l''a,W'⟩" by (blast intro: steps_z_alt)
  with ***(2,3) show ?case by blast
qed

text ‹Old proof using Bouyer's calculation›
lemma steps_z_alpha_closure_involutive'':
  "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',Z''⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V
  ⟹ ∃ Z'''. A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z'''⟩ ∧ Closure⇩α Z'' ⊆ Closure⇩α Z'''"
proof (induction A l Z l' Z' arbitrary: Z'' l'' rule: steps_z_alpha.induct, goal_cases)
  case refl from this(1) show ?case by blast
next
  case A: (2 A l Z l' Z' l'' Z'' Z''a l''a)
  from A(3) obtain 𝒵 where Z'': "Z'' = Closure⇩α 𝒵" "A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',𝒵⟩" by auto
  from A(2)[OF Z''(2) A(5,6)] obtain Z''' where Z''':
    "A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z'''⟩" "Closure⇩α 𝒵 ⊆ Closure⇩α Z'''"
  by auto
  from steps_z_alpha_V[OF A(1,6)] step_z_V[OF Z''(2)] have *: "𝒵 ⊆ V" by blast
  from A Z'' have "A ⊢ ⟨l'', Closure⇩α 𝒵⟩ ↝ ⟨l''a,Z''a⟩" by auto
  from calc[OF A(5) * this] obtain 𝒵' where **:
    "A ⊢ ⟨l'', 𝒵⟩ ↝ ⟨l''a,𝒵'⟩" "Z''a ⊆ Closure⇩α 𝒵'"
  by auto
  from steps_z_alpha_closure_involutive'_aux[OF this(1) Z'''(2) A(5) *] obtain W' where ***:
    "A ⊢ ⟨l'', Z'''⟩ ↝ ⟨l''a,W'⟩" "Closure⇩α 𝒵' ⊆ Closure⇩α W'"
  by auto
  with Z'''(1) have "A ⊢ ⟨l, Z⟩ ↝* ⟨l''a,W'⟩" by (blast intro: steps_z_alt)
  with closure_involutive'[OF **(2)] ***(2) show ?case by blast
qed

lemma steps_z_alpha_closure_involutive:
  "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V
  ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z''⟩ ∧ Closure⇩α Z' ⊆ Closure⇩α Z'' ∧ Z'' ⊆ Z'"
proof (induction A l Z l' Z' rule: steps_z_alpha.induct)
  case refl show ?case by blast
next
  case 2: (step A l Z l' Z' l'' Z'')
  then obtain Z''a where *: "A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',Z''a⟩" "Z'' = Closure⇩α Z''a" by auto
  from steps_z_alpha_closure_involutive'[OF 2(1) this(1) 2(4,5)] obtain Z''' where Z''':
    "A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z'''⟩" "Closure⇩α Z''a ⊆ Closure⇩α Z'''" "Z''' ⊆ Z''a" by blast
  have "Z''' ⊆ Z''" by (metis *(1,2) 2(1,5) Z'''(3) closure_subs step_z_V steps_z_alpha_V subset_trans) 
  with * closure_involutive Z''' show ?case by auto
qed

lemma steps_z_V:
  "A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ⊆ V"
apply (induction rule: steps_z.induct)
  apply blast
using step_z_V by metis

lemma steps_z_alpha_sound:
  "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ Z' ≠ {}
  ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z''⟩ ∧ Z'' ≠ {} ∧ Z'' ⊆ Z'"
proof goal_cases
  case 1
  from steps_z_alpha_closure_involutive[OF 1(1-3)] obtain Z'' where
    Z'': "A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z''⟩" "Closure⇩α Z' ⊆ Closure⇩α Z''" "Z'' ⊆ Z'"
    by blast
  with 1(4) cla_empty_iff[OF steps_z_alpha_V[OF 1(1)], OF 1(3)]
    cla_empty_iff[OF steps_z_V, OF this(1) 1(3)] have "Z'' ≠ {}" by auto
  with Z'' show ?case by auto
qed

lemma step_z_mono:
  "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ Z ⊆ W ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝ ⟨l',W'⟩ ∧ Z' ⊆ W'"
proof (cases rule: step_z.cases, assumption, goal_cases)
  case A: 1
  let ?W' = "(W ∩ {u. u ⊢ inv_of A l})⇧↑ ∩ {u. u ⊢ inv_of A l}"
  from A have "A ⊢ ⟨l, W⟩ ↝ ⟨l',?W'⟩" by auto
  moreover have "Z' ⊆ ?W'"
    apply (subst A(4))
    apply (rule subset_int_mono)
    apply (rule zone_delay_mono)
    apply (rule subset_int_mono)
    apply (rule A(2))
  done
  ultimately show ?thesis by auto
next
  case A: (2 g a r)
  let ?W' = "zone_set (W ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
  from A have "A ⊢ ⟨l, W⟩ ↝ ⟨l',?W'⟩" by auto
  moreover have "Z' ⊆ ?W'"
    apply (subst A(3))
    apply (rule subset_int_mono)
    apply (rule zone_set_mono)
    apply (rule subset_int_mono)
    apply (rule A(2))
  done
  ultimately show ?thesis by auto
qed

lemma step_z_alpha_mono:
  "A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l',Z'⟩ ⟹ Z ⊆ W ⟹ W ⊆ V ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇩α ⟨l',W'⟩ ∧ Z' ⊆ W'"
proof goal_cases
  case 1
  then obtain Z'' where *: "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z''⟩" "Z' = Closure⇩α Z''" by auto
  from step_z_mono[OF this(1) 1(2)] obtain W' where "A ⊢ ⟨l, W⟩ ↝ ⟨l',W'⟩" "Z'' ⊆ W'" by auto
  moreover with *(2) have "Z' ⊆ Closure⇩α W'" unfolding cla_def by auto
  ultimately show ?case by blast
qed

lemma steps_z_alpha_mono:
  "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z'⟩ ⟹ Z ⊆ W ⟹ W ⊆ V ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇩α* ⟨l',W'⟩ ∧ Z' ⊆ W'"
proof (induction rule: steps_z_alpha.induct, goal_cases)
  case refl then show ?case by auto
next
  case (2 A l Z l' Z' l'' Z'')
  then obtain W' where "A ⊢ ⟨l, W⟩ ↝⇩α* ⟨l',W'⟩" "Z' ⊆ W'" by auto
  with step_z_alpha_mono[OF 2(3) this(2) steps_z_alpha_V[OF this(1) 2(5)]]
  show ?case by blast
qed

lemma steps_z_alpha_alt:
  "A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l', Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝⇩α* ⟨l'', Z''⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l'', Z''⟩"
by (rotate_tac, induction rule: steps_z_alpha.induct) blast+

lemma steps_z_alpha_complete:
  "A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ Z' ≠ {}
  ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z''⟩ ∧ Z' ⊆ Z''"
proof (induction rule: steps_z.induct, goal_cases)
  case refl with cla_empty_iff show ?case by blast
next
  case (2 A l Z l' Z' l'' Z'')
  with step_z_V[OF this(1,5)] obtain Z''' where "A ⊢ ⟨l', Z'⟩ ↝⇩α* ⟨l'',Z'''⟩" "Z'' ⊆ Z'''" by blast
  with steps_z_alpha_mono[OF this(1) closure_subs[OF step_z_V[OF 2(1,5)]] closure_V]
  obtain W' where W': "A ⊢ ⟨l', Closure⇩α Z'⟩ ↝⇩α* ⟨l'',W'⟩" " Z'' ⊆ W'" by auto
  with 2(1) have "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l'',W'⟩" by (auto intro: steps_z_alpha_alt)
  with W' show ?case by auto
qed

lemma steps_z_alpha_complete':
  "A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ Z' ≠ {}
  ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z''⟩ ∧ Z'' ≠ {}"
using steps_z_alpha_complete by fast

end

end