Theory PDS

theory PDS imports "P_Automata" "HOL-Library.While_Combinator" begin


section ‹PDS›

datatype 'label operation = pop | swap 'label | push 'label 'label
type_synonym ('ctr_loc, 'label) rule = "('ctr_loc × 'label) × ('ctr_loc × 'label operation)"
type_synonym ('ctr_loc, 'label) conf = "'ctr_loc × 'label list"


text ‹We define push down systems.›

locale PDS =
  fixes Δ :: "('ctr_loc, 'label::finite) rule set"
  (* 'ctr_loc is the type of control locations *)
  
begin

primrec lbl :: "'label operation ⇒ 'label list" where
  "lbl pop = []"
| "lbl (swap γ) = [γ]" 
| "lbl (push γ  γ') = [γ, γ']"

definition is_rule :: "'ctr_loc × 'label ⇒ 'ctr_loc × 'label operation ⇒ bool" (infix "↪" 80) where
  "pγ ↪ p'w ≡ (pγ,p'w) ∈ Δ"

inductive_set transition_rel :: "(('ctr_loc, 'label) conf × unit × ('ctr_loc, 'label) conf) set" where
  "(p, γ) ↪ (p', w) ⟹ 
   ((p, γ#w'), (), (p', (lbl w)@w')) ∈ transition_rel"

interpretation LTS transition_rel .

notation step_relp (infix "⇒" 80)
notation step_starp (infix "⇒⇧*" 80)

lemma step_relp_def2:
  "(p, γw') ⇒ (p',ww') ⟷ (∃γ w' w. γw' = γ#w' ∧ ww' = (lbl w)@w' ∧ (p, γ) ↪ (p', w))"
  by (metis (no_types, lifting) PDS.transition_rel.intros step_relp_def transition_rel.cases)

end


section ‹PDS with P automata›

type_synonym ('ctr_loc, 'label) sat_rule = "('ctr_loc, 'label) transition set ⇒ ('ctr_loc, 'label) transition set ⇒ bool"

datatype ('ctr_loc, 'noninit, 'label) state =
  is_Init: Init (the_Ctr_Loc: 'ctr_loc) (* p ∈ P *)
  | is_Noninit: Noninit (the_St: 'noninit) (* q ∈ Q ∧ q ∉ P *)
  | is_Isolated: Isolated (the_Ctr_Loc: 'ctr_loc) (the_Label: 'label) (* q⇩p⇩γ *)

lemma finitely_many_states:
  assumes "finite (UNIV :: 'ctr_loc set)"
  assumes "finite (UNIV :: 'noninit set)"
  assumes "finite (UNIV :: 'label set)"
  shows "finite (UNIV :: ('ctr_loc, 'noninit, 'label) state set)"
proof -
  define Isolated' :: "('ctr_loc * 'label) ⇒ ('ctr_loc, 'noninit, 'label) state" where 
    "Isolated' == λ(c :: 'ctr_loc, l:: 'label). Isolated c l"
  define Init' :: "'ctr_loc ⇒ ('ctr_loc, 'noninit, 'label) state" where
    "Init' = Init"
  define Noninit' :: "'noninit ⇒ ('ctr_loc, 'noninit, 'label) state" where
    "Noninit' = Noninit"

  have split: "UNIV = (Init' ` UNIV) ∪ (Noninit' ` UNIV) ∪ (Isolated' ` (UNIV :: (('ctr_loc * 'label) set)))"
    unfolding Init'_def Noninit'_def
  proof (rule; rule; rule; rule)
    fix x :: "('ctr_loc, 'noninit, 'label) state"
    assume "x ∈ UNIV"
    moreover
    assume "x ∉ range Isolated'"
    moreover
    assume "x ∉ range Noninit"
    ultimately
    show "x ∈ range Init"
      by (metis Isolated'_def prod.simps(2) range_eqI state.exhaust)
  qed

  have "finite (Init' ` (UNIV:: 'ctr_loc set))"
    using assms by auto
  moreover
  have "finite (Noninit' ` (UNIV:: 'noninit set))"
    using assms by auto
  moreover
  have "finite (UNIV :: (('ctr_loc * 'label) set))"
    using assms by (simp add: finite_Prod_UNIV)
  then have "finite (Isolated' ` (UNIV :: (('ctr_loc * 'label) set)))"
    by auto
  ultimately
  show "finite (UNIV :: ('ctr_loc, 'noninit, 'label) state set)"
    unfolding split by auto
qed

instantiation state :: (finite, finite, finite) finite begin

instance by standard (simp add: finitely_many_states)

end


locale PDS_with_P_automata = PDS Δ
  for Δ :: "('ctr_loc::enum, 'label::finite) rule set"
    +
  fixes final_inits :: "('ctr_loc::enum) set"
  fixes final_noninits :: "('noninit::finite) set"
begin

(* Corresponds to Schwoon's F *)
definition finals :: "('ctr_loc, 'noninit::finite, 'label) state set" where
  "finals = Init ` final_inits ∪ Noninit ` final_noninits"

lemma F_not_Ext: "¬(∃f∈finals. is_Isolated f)"
  using finals_def by fastforce

(* Corresponds to Schwoon's P *)
definition inits :: "('ctr_loc, 'noninit, 'label) state set" where 
  "inits = {q. is_Init q}"

lemma inits_code[code]: "inits = set (map Init Enum.enum)"
  by (auto simp: inits_def is_Init_def simp flip: UNIV_enum)

definition noninits :: "('ctr_loc, 'noninit, 'label) state set" where
  "noninits = {q. is_Noninit q}"

definition isols :: "('ctr_loc, 'noninit, 'label) state set" where
  "isols = {q. is_Isolated q}"

sublocale LTS transition_rel .
notation step_relp (infix "⇒" 80)
notation step_starp (infix "⇒⇧*" 80)

definition accepts :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set ⇒ ('ctr_loc, 'label) conf ⇒ bool" where
  "accepts ts ≡ λ(p,w). (∃q ∈ finals. (Init p,w,q) ∈ LTS.trans_star ts)"

lemma accepts_accepts_aut: "accepts ts (p, w) ⟷ P_Automaton.accepts_aut ts Init finals p w"
  unfolding accepts_def P_Automaton.accepts_aut_def inits_def by auto

definition accepts_ε :: "(('ctr_loc, 'noninit, 'label) state, 'label option) transition set ⇒ ('ctr_loc, 'label) conf ⇒ bool" where
  "accepts_ε ts ≡ λ(p,w). (∃q ∈ finals. (Init p,w,q) ∈ LTS_ε.trans_star_ε ts)"

abbreviation ε :: "'label option" where
  "ε == None"

lemma accepts_mono[mono]: "mono accepts" 
proof (rule, rule)
  fix c :: "('ctr_loc, 'label) conf"
  fix ts ts' :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set"
  assume accepts_ts: "accepts ts c"
  assume tsts': "ts ⊆ ts'"
  obtain p l where pl_p: "c = (p,l)"
    by (cases c)
  obtain q where q_p:  "q ∈ finals ∧ (Init p, l, q) ∈ LTS.trans_star ts"
    using accepts_ts unfolding pl_p accepts_def by auto
  then have "(Init p, l, q) ∈ LTS.trans_star ts'"
    using tsts' LTS_trans_star_mono monoD by blast 
  then have "accepts ts' (p,l)"
    unfolding accepts_def using q_p by auto
  then show "accepts ts' c"
    unfolding pl_p .
qed

lemma accepts_cons: "(Init p, γ, Init p') ∈ ts ⟹ accepts ts (p', w) ⟹ accepts ts (p, γ # w)"
  using LTS.trans_star.trans_star_step accepts_def by fastforce 

definition lang :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set ⇒ ('ctr_loc, 'label) conf set" where
  "lang ts = {c. accepts ts c}"

lemma lang_lang_aut: "lang ts = (λ(s,w). (s, w)) ` (P_Automaton.lang_aut ts Init finals)"
  unfolding lang_def P_Automaton.lang_aut_def
  by (auto simp: inits_def accepts_def P_Automaton.accepts_aut_def image_iff intro!: exI[of _ "Init _"])

lemma lang_aut_lang: "P_Automaton.lang_aut ts Init finals = lang ts"
  unfolding lang_lang_aut
  by (auto 0 3 simp: P_Automaton.lang_aut_def P_Automaton.accepts_aut_def inits_def image_iff)

definition lang_ε :: "(('ctr_loc, 'noninit, 'label) state, 'label option) transition set ⇒ ('ctr_loc, 'label) conf set" where
  "lang_ε ts = {c. accepts_ε ts c}"


subsection ‹Saturations›

definition saturated :: "('c, 'l) sat_rule ⇒ ('c, 'l) transition set ⇒ bool" where
  "saturated rule ts ⟷ (∄ts'. rule ts ts')"

definition saturation :: "('c, 'l) sat_rule ⇒ ('c, 'l) transition set ⇒ ('c, 'l) transition set ⇒ bool" where
  "saturation rule ts ts' ⟷ rule⇧*⇧* ts ts' ∧ saturated rule ts'"

lemma no_infinite: 
  assumes "⋀ts ts' :: ('c ::finite, 'l::finite) transition set. rule ts ts' ⟹ card ts' = Suc (card ts)"
  assumes "∀i :: nat. rule (tts i) (tts (Suc i))"
  shows "False"
proof -
  define f where "f i = card (tts i)" for i
  have f_Suc: "∀i. f i < f (Suc i)"
    using assms f_def lessI by metis
  have "∀i. ∃j. f j > i"
  proof 
    fix i
    show "∃j. i < f j"
    proof(induction i)
      case 0
      then show ?case 
        by (metis f_Suc neq0_conv)
    next
      case (Suc i)
      then show ?case
        by (metis Suc_lessI f_Suc)
    qed
  qed
  then have "∃j. f j > card (UNIV :: ('c, 'l) transition set)"
    by auto
  then show False
    by (metis card_seteq f_def finite_UNIV le_eq_less_or_eq nat_neq_iff subset_UNIV)
qed

lemma saturation_termination:
  assumes "⋀ts ts' :: ('c ::finite, 'l::finite) transition set. rule ts ts' ⟹ card ts' = Suc (card ts)"
  shows "¬(∃tts. (∀i :: nat. rule (tts i) (tts (Suc i))))"
  using assms no_infinite by blast 

lemma saturation_exi: 
  assumes "⋀ts ts' :: ('c ::finite, 'l::finite) transition set. rule ts ts' ⟹ card ts' = Suc (card ts)"
  shows "∃ts'. saturation rule ts ts'"
proof (rule ccontr)
  assume a: "∄ts'. saturation rule ts ts'"
  define g where "g ts = (SOME ts'. rule ts ts')" for ts
  define tts where "tts i = (g ^^ i) ts" for i
  have "∀i :: nat. rule⇧*⇧* ts (tts i) ∧ rule (tts i) (tts (Suc i))"
  proof 
    fix i
    show "rule⇧*⇧* ts (tts i) ∧ rule (tts i) (tts (Suc i))"
    proof (induction i)
      case 0
      have "rule ts (g ts)"
        by (metis g_def a rtranclp.rtrancl_refl saturation_def saturated_def someI)
      then show ?case
        using tts_def a saturation_def by auto 
    next
      case (Suc i)
      then have sat_Suc: "rule⇧*⇧* ts (tts (Suc i))"
        by fastforce
      then have "rule (g ((g ^^ i) ts)) (g (g ((g ^^ i) ts)))"
        by (metis Suc.IH tts_def g_def a r_into_rtranclp rtranclp_trans saturation_def saturated_def 
            someI)
      then have "rule (tts (Suc i)) (tts (Suc (Suc i)))"
        unfolding tts_def by simp
      then show ?case
        using sat_Suc by auto
    qed
  qed
  then have "∀i. rule (tts i) (tts (Suc i))"
    by auto
  then show False
    using no_infinite assms by auto
qed


subsection ‹Saturation rules›

inductive pre_star_rule :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set ⇒ (('ctr_loc, 'noninit, 'label) state, 'label) transition set ⇒ bool" where 
  add_trans: "(p, γ) ↪ (p', w) ⟹ (Init p', lbl w, q) ∈ LTS.trans_star ts ⟹
    (Init p, γ, q) ∉ ts ⟹ pre_star_rule ts (ts ∪ {(Init p, γ, q)})"

definition pre_star1 :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set ⇒ (('ctr_loc, 'noninit, 'label) state, 'label) transition set" where
  "pre_star1 ts =
    (⋃((p, γ), (p', w)) ∈ Δ. ⋃q ∈ LTS.reach ts (Init p') (lbl w). {(Init p, γ, q)})"

lemma pre_star1_mono: "mono pre_star1"
  unfolding pre_star1_def
  by (auto simp: mono_def LTS.trans_star_code[symmetric] elim!: bexI[rotated]
    LTS_trans_star_mono[THEN monoD, THEN subsetD])

lemma pre_star_rule_pre_star1:
  assumes "X ⊆ pre_star1 ts"
  shows "pre_star_rule⇧*⇧* ts (ts ∪ X)"
proof -
  have "finite X"
    by simp
  from this assms show ?thesis
  proof (induct X arbitrary: ts rule: finite_induct)
    case (insert x F)
    then obtain p γ p' w q where *: "(p, γ) ↪ (p', w)" 
      "(Init p', lbl w, q) ∈ LTS.trans_star ts" and x:
      "x = (Init p, γ, q)"
      by (auto simp: pre_star1_def is_rule_def LTS.trans_star_code)
    with insert show ?case
    proof (cases "(Init p, γ, q) ∈ ts")
      case False
      with insert(1,2,4) x show ?thesis
        by (intro converse_rtranclp_into_rtranclp[of pre_star_rule, OF add_trans[OF * False]])
          (auto intro!: insert(3)[of "insert x ts", simplified x Un_insert_left]
            intro: pre_star1_mono[THEN monoD, THEN set_mp, of ts])
    qed (simp add: insert_absorb)
  qed simp
qed

lemma pre_star_rule_pre_star1s: "pre_star_rule⇧*⇧* ts (((λs. s ∪ pre_star1 s) ^^ k) ts)"
  by (induct k) (auto elim!: rtranclp_trans intro: pre_star_rule_pre_star1)

definition "pre_star_loop = while_option (λs. s ∪ pre_star1 s ≠ s) (λs. s ∪ pre_star1 s)"
definition "pre_star_exec = the o pre_star_loop"
definition "pre_star_exec_check A = (if inits ⊆ LTS.srcs A then pre_star_loop A else None)"

definition "accept_pre_star_exec_check A c = (if inits ⊆ LTS.srcs A then Some (accepts (pre_star_exec A) c) else None)"

lemma while_option_finite_subset_Some: fixes C :: "'a set"
  assumes "mono f" and "!!X. X ⊆ C ⟹ f X ⊆ C" and "finite C" and X: "X ⊆ C" "X ⊆ f X"
  shows "∃P. while_option (λA. f A ≠ A) f X = Some P"
proof(rule measure_while_option_Some[where
    f= "%A::'a set. card C - card A" and P= "%A. A ⊆ C ∧ A ⊆ f A" and s= X])
  fix A assume A: "A ⊆ C ∧ A ⊆ f A" "f A ≠ A"
  show "(f A ⊆ C ∧ f A ⊆ f (f A)) ∧ card C - card (f A) < card C - card A"
    (is "?L ∧ ?R")
  proof
    show ?L by(metis A(1) assms(2) monoD[OF ‹mono f›])
    show ?R 
      by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear 
          rev_finite_subset)
  qed
qed (simp add: X)

lemma pre_star_exec_terminates: "∃t. pre_star_loop s = Some t"
  unfolding pre_star_loop_def
  by (rule while_option_finite_subset_Some[where C=UNIV])
    (auto simp: mono_def dest: pre_star1_mono[THEN monoD])

lemma pre_star_exec_code[code]:
  "pre_star_exec s = (let s' = pre_star1 s in if s' ⊆ s then s else pre_star_exec (s ∪ s'))"
  unfolding pre_star_exec_def pre_star_loop_def o_apply
  by (subst while_option_unfold)(auto simp: Let_def)

lemma saturation_pre_star_exec: "saturation pre_star_rule ts (pre_star_exec ts)"
proof -
  from pre_star_exec_terminates obtain t where t: "pre_star_loop ts = Some t"
    by blast
  obtain k where k: "t = ((λs. s ∪ pre_star1 s) ^^ k) ts" and le: "pre_star1 t ⊆ t"
    using while_option_stop2[OF t[unfolded pre_star_loop_def]] by auto
  have "(⋃{us. pre_star_rule t us}) - t ⊆ pre_star1 t"
    by (auto simp: pre_star1_def LTS.trans_star_code[symmetric] prod.splits is_rule_def
      pre_star_rule.simps)
  from subset_trans[OF this le] show ?thesis
    unfolding saturation_def saturated_def pre_star_exec_def o_apply k t
    by (auto 9 0 simp: pre_star_rule_pre_star1s subset_eq pre_star_rule.simps)
qed

inductive post_star_rules :: "(('ctr_loc, 'noninit, 'label) state, 'label option) transition set ⇒ (('ctr_loc, 'noninit, 'label) state, 'label option) transition set ⇒ bool" where
  add_trans_pop: 
  "(p, γ) ↪ (p', pop) ⟹ 
   (Init p, [γ], q) ∈ LTS_ε.trans_star_ε ts ⟹ 
   (Init p', ε, q) ∉ ts ⟹ 
   post_star_rules ts (ts ∪ {(Init p', ε, q)})"
| add_trans_swap: 
  "(p, γ) ↪ (p', swap γ') ⟹ 
   (Init p, [γ], q) ∈ LTS_ε.trans_star_ε ts ⟹ 
   (Init p', Some γ', q) ∉ ts ⟹ 
   post_star_rules ts (ts ∪ {(Init p', Some γ', q)})"
| add_trans_push_1: 
  "(p, γ) ↪ (p', push γ' γ'') ⟹ 
   (Init p, [γ], q) ∈ LTS_ε.trans_star_ε ts ⟹ 
   (Init p', Some γ', Isolated p' γ') ∉ ts ⟹ 
   post_star_rules ts (ts ∪ {(Init p', Some γ', Isolated p' γ')})"
| add_trans_push_2: 
  "(p, γ) ↪ (p', push γ' γ'') ⟹ 
   (Init p, [γ], q) ∈ LTS_ε.trans_star_ε ts ⟹ 
   (Isolated p' γ', Some γ'', q) ∉ ts ⟹ 
   (Init p', Some γ', Isolated p' γ') ∈ ts ⟹ 
   post_star_rules ts (ts ∪ {(Isolated p' γ', Some γ'', q)})"

lemma pre_star_rule_mono:
  "pre_star_rule ts ts' ⟹ ts ⊂ ts'"
  unfolding pre_star_rule.simps by auto

lemma post_star_rules_mono:
  "post_star_rules ts ts' ⟹ ts ⊂ ts'"
proof(induction rule: post_star_rules.induct)
  case (add_trans_pop p γ p' q ts)
  then show ?case by auto
next
  case (add_trans_swap p γ p' γ' q ts)
  then show ?case by auto
next
  case (add_trans_push_1 p γ p' γ' γ'' q ts)
  then show ?case by auto
next
  case (add_trans_push_2 p γ p' γ' γ'' q ts)
  then show ?case by auto
qed

lemma pre_star_rule_card_Suc: "pre_star_rule ts ts' ⟹ card ts' = Suc (card ts)"
  unfolding pre_star_rule.simps by auto

lemma post_star_rules_card_Suc: "post_star_rules ts ts' ⟹ card ts' = Suc (card ts)"
proof(induction rule: post_star_rules.induct)
  case (add_trans_pop p γ p' q ts)
  then show ?case by auto
next
  case (add_trans_swap p γ p' γ' q ts)
  then show ?case by auto
next
  case (add_trans_push_1 p γ p' γ' γ'' q ts)
  then show ?case by auto
next
  case (add_trans_push_2 p γ p' γ' γ'' q ts)
  then show ?case by auto
qed


lemma pre_star_saturation_termination: 
  "¬(∃tts. (∀i :: nat. pre_star_rule (tts i) (tts (Suc i))))"
  using no_infinite pre_star_rule_card_Suc by blast 

lemma post_star_saturation_termination: 
  "¬(∃tts. (∀i :: nat. post_star_rules (tts i) (tts (Suc i))))"
  using no_infinite post_star_rules_card_Suc by blast

lemma pre_star_saturation_exi: 
  shows "∃ts'. saturation pre_star_rule ts ts'"
  using pre_star_rule_card_Suc saturation_exi by blast

lemma post_star_saturation_exi: 
  shows "∃ts'. saturation post_star_rules ts ts'"
  using post_star_rules_card_Suc saturation_exi by blast

lemma pre_star_rule_incr: "pre_star_rule A B ⟹ A ⊆ B"
proof(induction rule: pre_star_rule.inducts)
  case (add_trans p γ p' w q rel)
  then show ?case 
    by auto
qed

lemma post_star_rules_incr: "post_star_rules A B ⟹ A ⊆ B"
proof(induction rule: post_star_rules.inducts)
  case (add_trans_pop p γ p' q ts)
  then show ?case
    by auto
next
  case (add_trans_swap p γ p' γ' q ts)
  then show ?case 
    by auto
next
  case (add_trans_push_1 p γ p' γ' γ'' q ts)
  then show ?case 
    by auto
next
  case (add_trans_push_2 p γ p' γ' γ'' q ts)
  then show ?case 
    by auto
qed

lemma saturation_rtranclp_pre_star_rule_incr: "pre_star_rule⇧*⇧* A B ⟹ A ⊆ B"
proof (induction rule: rtranclp_induct)
  case base
  then show ?case by auto
next
  case (step y z)
  then show ?case
    using pre_star_rule_incr by auto
qed

lemma saturation_rtranclp_post_star_rule_incr: "post_star_rules⇧*⇧* A B ⟹ A ⊆ B"
proof (induction rule: rtranclp_induct)
  case base
  then show ?case by auto
next
  case (step y z)
  then show ?case
    using post_star_rules_incr by auto
qed

lemma pre_star'_incr_trans_star:
  "pre_star_rule⇧*⇧* A A' ⟹ LTS.trans_star A ⊆ LTS.trans_star A'"
  using mono_def LTS_trans_star_mono saturation_rtranclp_pre_star_rule_incr by metis

lemma post_star'_incr_trans_star:
  "post_star_rules⇧*⇧* A A' ⟹ LTS.trans_star A ⊆ LTS.trans_star A'"
  using mono_def LTS_trans_star_mono saturation_rtranclp_post_star_rule_incr by metis

lemma post_star'_incr_trans_star_ε:
  "post_star_rules⇧*⇧* A A' ⟹ LTS_ε.trans_star_ε A ⊆ LTS_ε.trans_star_ε A'"
  using mono_def LTS_ε_trans_star_ε_mono saturation_rtranclp_post_star_rule_incr by metis

lemma pre_star_lim'_incr_trans_star:
  "saturation pre_star_rule A A' ⟹ LTS.trans_star A ⊆ LTS.trans_star A'"
  by (simp add: pre_star'_incr_trans_star saturation_def)

lemma post_star_lim'_incr_trans_star:
  "saturation post_star_rules A A' ⟹ LTS.trans_star A ⊆ LTS.trans_star A'"
  by (simp add: post_star'_incr_trans_star saturation_def)

lemma post_star_lim'_incr_trans_star_ε:
  "saturation post_star_rules A A' ⟹ LTS_ε.trans_star_ε A ⊆ LTS_ε.trans_star_ε A'"
  by (simp add: post_star'_incr_trans_star_ε saturation_def)


subsection ‹Pre* lemmas›

lemma inits_srcs_iff_Ctr_Loc_srcs:
  "inits ⊆ LTS.srcs A ⟷ (∄q γ q'. (q, γ, Init q') ∈ A)"
proof 
  assume "inits ⊆ LTS.srcs A"
  then show "∄q γ q'. (q, γ, Init q') ∈ A"
    by (simp add: Collect_mono_iff LTS.srcs_def inits_def)
next
  assume "∄q γ q'. (q, γ, Init q') ∈ A"
  show "inits ⊆ LTS.srcs A"
    by (metis LTS.srcs_def2 inits_def ‹∄q γ q'. (q, γ, Init q') ∈ A› mem_Collect_eq 
        state.collapse(1) subsetI)
qed

lemma lemma_3_1:
  assumes "p'w ⇒⇧* pv"
  assumes "pv ∈ lang A"
  assumes "saturation pre_star_rule A A'"
  shows "accepts A' p'w"
  using assms
proof (induct rule: converse_rtranclp_induct)
  case base
  define p where "p = fst pv"
  define v where "v = snd pv"
  from base have "∃q ∈ finals. (Init p, v, q) ∈ LTS.trans_star A'"
    unfolding lang_def p_def v_def using pre_star_lim'_incr_trans_star accepts_def by fastforce 
  then show ?case
    unfolding accepts_def p_def v_def by auto
next
  case (step p'w p''u) 
  define p' where "p' = fst p'w"
  define w  where "w = snd p'w"
  define p'' where "p'' = fst p''u"
  define u  where "u = snd p''u"
  have p'w_def: "p'w = (p', w)"
    using p'_def w_def by auto
  have p''u_def: "p''u = (p'', u)"
    using p''_def u_def by auto

  then have "accepts A' (p'', u)" 
    using step by auto
  then obtain q where q_p: "q ∈ finals ∧ (Init p'', u, q) ∈ LTS.trans_star A'"
    unfolding accepts_def by auto
  have "∃γ w1 u1. w=γ#w1 ∧ u=lbl u1@w1 ∧ (p', γ) ↪ (p'', u1)"
    using p''u_def p'w_def step.hyps(1) step_relp_def2 by auto
  then obtain γ w1 u1 where γ_w1_u1_p: "w=γ#w1 ∧ u=lbl u1@w1 ∧ (p', γ) ↪ (p'', u1)"
    by blast

  then have "∃q1. (Init p'', lbl u1, q1) ∈ LTS.trans_star A' ∧ (q1, w1, q) ∈ LTS.trans_star A'"
    using q_p LTS.trans_star_split by auto

  then obtain q1 where q1_p: "(Init p'', lbl u1, q1) ∈ LTS.trans_star A' ∧ (q1, w1, q) ∈ LTS.trans_star A'"
    by auto

  then have in_A': "(Init p', γ, q1) ∈ A'"
    using γ_w1_u1_p add_trans[of p' γ p'' u1 q1 A'] saturated_def saturation_def step.prems by metis

  then have "(Init p', γ#w1, q) ∈ LTS.trans_star A'"
    using LTS.trans_star.trans_star_step q1_p by meson
  then have t_in_A': "(Init p', w, q) ∈ LTS.trans_star A'"
    using γ_w1_u1_p by blast

  from q_p t_in_A' have "q ∈ finals ∧ (Init p', w, q) ∈ LTS.trans_star A'"
    by auto
  then show ?case
    unfolding accepts_def p'w_def by auto 
qed

lemma word_into_init_empty_states:
  fixes A :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set"
  assumes "(p, w, ss, Init q) ∈ LTS.trans_star_states A"
  assumes "inits ⊆ LTS.srcs A"
  shows "w = [] ∧ p = Init q ∧ ss=[p]"
proof -
  define q1 :: "('ctr_loc, 'noninit, 'label) state" where 
    "q1 = Init q"
  have q1_path: "(p, w, ss, q1) ∈ LTS.trans_star_states A"
    by (simp add: assms(1) q1_def)
  moreover
  have "q1 ∈ inits"
    by (simp add: inits_def q1_def)
  ultimately
  have "w = [] ∧ p = q1 ∧ ss=[p]"
  proof(induction rule: LTS.trans_star_states.induct[OF q1_path])
    case (1 p)
    then show ?case by auto
  next
    case (2 p γ q' w ss q)
    have "∄q γ q'. (q, γ, Init q') ∈ A"
      using assms(2) unfolding inits_def LTS.srcs_def by (simp add: Collect_mono_iff) 
    then show ?case
      using 2 assms(2) by (metis inits_def is_Init_def mem_Collect_eq)
  qed
  then show ?thesis
    using q1_def by fastforce
qed

(* This corresponds to and slightly generalizes Schwoon's lemma 3.2(b) *)
lemma word_into_init_empty:
  fixes A :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set"
  assumes "(p, w, Init q) ∈ LTS.trans_star A"
  assumes "inits ⊆ LTS.srcs A"
  shows "w = [] ∧ p = Init q"
  using assms word_into_init_empty_states LTS.trans_star_trans_star_states by metis

lemma step_relp_append_aux:
  assumes "pu ⇒⇧* p1y"
  shows "(fst pu, snd pu @ v) ⇒⇧* (fst p1y, snd p1y @ v)"
  using assms 
proof (induction rule: rtranclp_induct)
  case base
  then show ?case by auto
next
  case (step p'w p1y)
  define p where "p = fst pu"
  define u where "u = snd pu"
  define p' where "p' = fst p'w"
  define w where "w = snd p'w"
  define p1 where "p1 = fst p1y"
  define y where "y = snd p1y"
  have step_1: "(p,u) ⇒⇧* (p',w)"
    by (simp add: p'_def p_def step.hyps(1) u_def w_def)
  have step_2: "(p',w) ⇒ (p1,y)"
    by (simp add: p'_def p1_def step.hyps(2) w_def y_def)
  have step_3: "(p, u @ v) ⇒⇧* (p', w @ v)"
    by (simp add: p'_def p_def step.IH u_def w_def)

  note step' = step_1 step_2 step_3

  from step'(2) have "∃γ w' wa. w = γ # w' ∧ y = lbl wa @ w' ∧ (p', γ) ↪ (p1, wa)"
    using step_relp_def2[of p' w p1 y] by auto
  then obtain γ w' wa where γ_w'_wa_p: " w = γ # w' ∧ y = lbl wa @ w' ∧ (p', γ) ↪ (p1, wa)"
    by metis
  then have "(p, u @ v) ⇒⇧* (p1, y @ v)"
    by (metis (no_types, lifting) PDS.step_relp_def2 append.assoc append_Cons rtranclp.simps step_3)
  then show ?case
    by (simp add: p1_def p_def u_def y_def)
qed

lemma step_relp_append:
  assumes "(p, u) ⇒⇧* (p1, y)"
  shows "(p, u @ v) ⇒⇧* (p1, y @ v)"
  using assms step_relp_append_aux by auto

lemma step_relp_append_empty:
  assumes "(p, u) ⇒⇧* (p1, [])"
  shows "(p, u @ v) ⇒⇧* (p1, v)"
  using step_relp_append[OF assms] by auto

lemma lemma_3_2_a':
  assumes "inits ⊆ LTS.srcs A"
  assumes "pre_star_rule⇧*⇧* A A'"
  assumes "(Init p, w, q) ∈ LTS.trans_star A'"
  shows "∃p' w'. (Init p', w', q) ∈ LTS.trans_star A ∧ (p, w) ⇒⇧* (p', w')"
  using assms(2) assms(3)
proof (induction arbitrary: p q w rule: rtranclp_induct)
  case base
  then have "(Init p, w, q) ∈ LTS.trans_star A ∧ (p, w) ⇒⇧* (p, w)"
    by auto
  then show ?case
    by auto
next
  case (step Aiminus1 Ai)

  from step(2) obtain p1 γ p2 w2 q' where p1_γ_p2_w2_q'_p:
    "Ai = Aiminus1 ∪ {(Init p1, γ, q')}"
    "(p1, γ) ↪ (p2, w2)"
    "(Init p2, lbl w2, q') ∈ LTS.trans_star Aiminus1"
    "(Init p1, γ, q') ∉ Aiminus1"
    by (meson pre_star_rule.cases)

  define t :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition"
    where "t = (Init p1, γ, q')"

  obtain ss where ss_p: "(Init p, w, ss, q) ∈ LTS.trans_star_states Ai"
    using step(4) LTS.trans_star_trans_star_states by metis

  define j where "j = count (transitions_of' (Init p, w, ss, q)) t"

  from j_def ss_p show ?case
  proof (induction j arbitrary: p q w ss)
    case 0
    then have "(Init p, w, q) ∈ LTS.trans_star Aiminus1"
      using count_zero_remove_trans_star_states_trans_star p1_γ_p2_w2_q'_p(1) t_def by metis
    then show ?case
      using step.IH by metis
  next
    case (Suc j')
    have "∃u v u_ss v_ss.
            ss = u_ss@v_ss ∧ w = u@[γ]@v ∧
            (Init p,u,u_ss, Init p1) ∈ LTS.trans_star_states Aiminus1 ∧
            (Init p1,[γ],q') ∈ LTS.trans_star Ai ∧
            (q',v,v_ss,q) ∈ LTS.trans_star_states Ai ∧
            (Init p, w, ss, q) = ((Init p, u, u_ss, Init p1), γ) @@⇧γ (q', v, v_ss, q)"
      using split_at_first_t[of "Init p" w ss q Ai j' "Init p1" γ q' Aiminus1]
      using Suc(2,3) t_def  p1_γ_p2_w2_q'_p(1,4) t_def by auto
    then obtain u v u_ss v_ss where u_v_u_ss_v_ss_p:
      "ss = u_ss@v_ss ∧ w = u@[γ]@v"
      "(Init p,u,u_ss, Init p1) ∈ LTS.trans_star_states Aiminus1"
      "(Init p1,[γ],q') ∈ LTS.trans_star Ai"
      "(q',v,v_ss,q) ∈ LTS.trans_star_states Ai"
      "(Init p, w, ss, q) = ((Init p, u, u_ss, Init p1), γ) @@⇧γ (q', v, v_ss, q)"
      by blast
    from this(2) have "∃p'' w''. (Init p'', w'', Init p1) ∈ LTS.trans_star A ∧ (p, u) ⇒⇧* (p'', w'')"
      using Suc(1)[of p u _ "Init p1"] step.IH step.prems(1)
      by (meson LTS.trans_star_states_trans_star LTS.trans_star_trans_star_states) 
    from this this(1) have VIII: "(p, u) ⇒⇧* (p1, [])"
      using word_into_init_empty assms(1) by blast

    note IX = p1_γ_p2_w2_q'_p(2)
    note III = p1_γ_p2_w2_q'_p(3)
    from III have III_2: "∃w2_ss. (Init p2, lbl w2, w2_ss, q') ∈ LTS.trans_star_states Aiminus1"
      using LTS.trans_star_trans_star_states[of "Init p2" "lbl w2" q' Aiminus1] by auto
    then obtain w2_ss where III_2: "(Init p2, lbl w2, w2_ss, q') ∈ LTS.trans_star_states Aiminus1"
      by blast

    from III have V: 
      "(Init p2, lbl w2, w2_ss, q') ∈ LTS.trans_star_states Aiminus1" 
      "(q', v, v_ss, q) ∈ LTS.trans_star_states Ai"
      using III_2 ‹(q', v, v_ss, q) ∈ LTS.trans_star_states Ai› by auto

    define w2v where "w2v = lbl w2 @ v"
    define w2v_ss where "w2v_ss = w2_ss @ tl v_ss"

    from V(1) have "(Init p2, lbl w2, w2_ss, q') ∈ LTS.trans_star_states Ai"
      using trans_star_states_mono p1_γ_p2_w2_q'_p(1) using Un_iff subsetI by (metis (no_types))
    then have V_merged: "(Init p2, w2v, w2v_ss, q) ∈ LTS.trans_star_states Ai"
      using V(2) unfolding w2v_def w2v_ss_def by (meson LTS.trans_star_states_append)

    have j'_count: "j' = count (transitions_of' (Init p2, w2v, w2v_ss, q)) t"
    proof -
      define countts where
        "countts == λx. count (transitions_of' x) t"

      have "countts (Init p, w, ss, q) = Suc j' "
        using Suc.prems(1) countts_def by force
      moreover
      have "countts (Init p, u, u_ss, Init p1) = 0"
        using LTS.avoid_count_zero countts_def p1_γ_p2_w2_q'_p(4) t_def u_v_u_ss_v_ss_p(2) 
        by fastforce
      moreover
      from u_v_u_ss_v_ss_p(5) have "countts (Init p, w, ss, q) = countts (Init p, u, u_ss, Init p1) + 1 + countts (q', v, v_ss, q)"
        using count_combine_trans_star_states countts_def t_def u_v_u_ss_v_ss_p(2) 
          u_v_u_ss_v_ss_p(4) by fastforce
      ultimately
      have "Suc j' = 0 + 1 + countts (q', v, v_ss, q)"
        by auto
      then have "j' = countts (q', v, v_ss, q)"
        by auto
      moreover
      have "countts (Init p2, lbl w2, w2_ss, q') = 0"
        using III_2 LTS.avoid_count_zero countts_def p1_γ_p2_w2_q'_p(4) t_def by fastforce
      moreover
      have "(Init p2, w2v, w2v_ss, q) = (Init p2, lbl w2, w2_ss, q') @@´ (q', v, v_ss, q)"
        using w2v_def w2v_ss_def by auto
      then have "countts (Init p2, w2v, w2v_ss, q) = countts (Init p2, lbl w2, w2_ss, q') + countts (q', v, v_ss, q)"
        using ‹(Init p2, lbl w2, w2_ss, q') ∈ LTS.trans_star_states Ai› 
          count_append_trans_star_states countts_def t_def u_v_u_ss_v_ss_p(4) by fastforce
      ultimately
      show ?thesis
        by (simp add: countts_def)
    qed

    have "∃p' w'. (Init p', w', q) ∈ LTS.trans_star A ∧ (p2, w2v) ⇒⇧* (p', w')"
      using Suc(1) using j'_count V_merged by auto
    then obtain p' w' where p'_w'_p: "(Init p', w', q) ∈ LTS.trans_star A" "(p2, w2v) ⇒⇧* (p', w')"
      by blast

    note X = p'_w'_p(2)

    have "(p,w) = (p,u@[γ]@v)"
      using ‹ss = u_ss @ v_ss ∧ w = u @ [γ] @ v› by blast

    have "(p,u@[γ]@v) ⇒⇧* (p1,γ#v)"
      using VIII step_relp_append_empty by auto

    from X have "(p1,γ#v) ⇒ (p2, w2v)"
      by (metis IX LTS.step_relp_def transition_rel.intros w2v_def)

    from X have
      "(p2, w2v) ⇒⇧* (p', w')"
      by simp

    have "(p, w) ⇒⇧* (p', w')"
      using X ‹(p, u @ [γ] @ v) ⇒⇧* (p1, γ # v)› ‹(p, w) = (p, u @ [γ] @ v)› ‹(p1, γ # v) ⇒ (p2, w2v)› by auto

    then have "(Init p', w', q) ∈ LTS.trans_star A ∧ (p, w) ⇒⇧* (p', w')"
      using p'_w'_p(1) by auto
    then show ?case
      by metis
  qed
qed 

lemma lemma_3_2_a:
  assumes "inits ⊆ LTS.srcs A"
  assumes "saturation pre_star_rule A A'"
  assumes "(Init p, w, q) ∈ LTS.trans_star A'"
  shows "∃p' w'. (Init p', w', q) ∈ LTS.trans_star A ∧ (p, w) ⇒⇧* (p', w')"
  using assms lemma_3_2_a' saturation_def by metis

― ‹Corresponds to one direction of Schwoon's theorem 3.2›
theorem pre_star_rule_subset_pre_star_lang:
  assumes "inits ⊆ LTS.srcs A"
  assumes "pre_star_rule⇧*⇧* A A'"
  shows "{c. accepts A' c} ⊆ pre_star (lang A)"
proof
  fix c :: "'ctr_loc × 'label list"
  assume c_a: "c ∈ {w. accepts A' w}"
  define p where "p = fst c"
  define w where "w = snd c"
  from p_def w_def c_a have "accepts A' (p,w)"
    by auto
  then have "∃q ∈ finals. (Init p, w, q) ∈ LTS.trans_star A'"
    unfolding accepts_def by auto
  then obtain q where q_p: "q ∈ finals" "(Init p, w, q) ∈ LTS.trans_star A'"
    by auto
  then have "∃p' w'. (p,w) ⇒⇧* (p',w') ∧ (Init p', w', q) ∈ LTS.trans_star A"
    using lemma_3_2_a' assms(1) assms(2) by metis
  then obtain p' w' where p'_w'_p: "(p,w) ⇒⇧* (p',w')" "(Init p', w', q) ∈ LTS.trans_star A"
    by auto
  then have "(p', w') ∈ lang A"
    unfolding lang_def unfolding accepts_def using q_p(1) by auto
  then have "(p,w) ∈ pre_star (lang A)"
    unfolding pre_star_def using p'_w'_p(1) by auto
  then show "c ∈ pre_star (lang A)"
    unfolding p_def w_def by auto
qed

― ‹Corresponds to Schwoon's theorem 3.2›
theorem pre_star_rule_accepts_correct:
  assumes "inits ⊆ LTS.srcs A"
  assumes "saturation pre_star_rule A A'"
  shows "{c. accepts A' c} = pre_star (lang A)"
proof (rule; rule)
  fix c :: "'ctr_loc × 'label list"
  define p where "p = fst c"
  define w where "w = snd c"
  assume "c ∈ pre_star (lang A)"
  then have "(p,w) ∈ pre_star (lang A)"
    unfolding p_def w_def by auto
  then have "∃p' w'. (p',w') ∈ lang A ∧ (p,w) ⇒⇧* (p',w')"
    unfolding pre_star_def by force
  then obtain p' w' where "(p',w') ∈ lang A ∧ (p,w) ⇒⇧* (p',w')"
    by auto
  then have "∃q ∈ finals. (Init p, w, q) ∈ LTS.trans_star A'"
    using lemma_3_1 assms(2) unfolding accepts_def by force
  then have "accepts A' (p,w)"
    unfolding accepts_def by auto
  then show "c ∈ {c. accepts A' c}"
    using p_def w_def by auto
next
  fix c :: "'ctr_loc × 'label list"
  assume "c ∈ {w. accepts A' w}"
  then show "c ∈ pre_star (lang A)"
    using pre_star_rule_subset_pre_star_lang assms unfolding saturation_def by auto
qed

― ‹Corresponds to Schwoon's theorem 3.2›
theorem pre_star_rule_correct:
  assumes "inits ⊆ LTS.srcs A"
  assumes "saturation pre_star_rule A A'"
  shows "lang A' = pre_star (lang A)"
  using assms(1) assms(2) lang_def pre_star_rule_accepts_correct by auto

theorem pre_star_exec_accepts_correct:
  assumes "inits ⊆ LTS.srcs A"
  shows "{c. accepts (pre_star_exec A) c} = pre_star (lang A)"
  using pre_star_rule_accepts_correct[of A "pre_star_exec A"] saturation_pre_star_exec[of A] 
    assms by auto

theorem pre_star_exec_lang_correct:
  assumes "inits ⊆ LTS.srcs A"
  shows "lang (pre_star_exec A) = pre_star (lang A)"
  using pre_star_rule_correct[of A "pre_star_exec A"] saturation_pre_star_exec[of A] assms by auto

theorem pre_star_exec_check_accepts_correct:
  assumes "pre_star_exec_check A ≠ None"
  shows "{c. accepts (the (pre_star_exec_check A)) c} = pre_star (lang A)"
  using pre_star_exec_accepts_correct assms unfolding pre_star_exec_check_def pre_star_exec_def
  by (auto split: if_splits)

theorem pre_star_exec_check_correct:
  assumes "pre_star_exec_check A ≠ None"
  shows "lang (the (pre_star_exec_check A)) = pre_star (lang A)"
  using pre_star_exec_check_accepts_correct assms unfolding lang_def by auto

theorem accept_pre_star_exec_correct_True:
  assumes "inits ⊆ LTS.srcs A"
  assumes "accepts (pre_star_exec A) c"
  shows "c ∈ pre_star (lang A)"
  using pre_star_exec_accepts_correct assms(1) assms(2) by blast

theorem accept_pre_star_exec_correct_False:
  assumes "inits ⊆ LTS.srcs A"
  assumes "¬accepts (pre_star_exec A) c"
  shows "c ∉ pre_star (lang A)"
  using pre_star_exec_accepts_correct assms(1) assms(2) by blast

theorem accept_pre_star_exec_correct_Some_True:
  assumes "accept_pre_star_exec_check A c = Some True"
  shows "c ∈ pre_star (lang A)"
proof -
  have "inits ⊆ LTS.srcs A"
    using assms unfolding accept_pre_star_exec_check_def
    by (auto split: if_splits)
  moreover
  have "accepts (pre_star_exec A) c"
    using assms
    using accept_pre_star_exec_check_def calculation by auto
  ultimately
  show "c ∈ pre_star (lang A)"
    using accept_pre_star_exec_correct_True by auto
qed

theorem accept_pre_star_exec_correct_Some_False:
  assumes "accept_pre_star_exec_check A c = Some False"
  shows "c ∉ pre_star (lang A)"
proof -
  have "inits ⊆ LTS.srcs A"
    using assms unfolding accept_pre_star_exec_check_def
    by (auto split: if_splits)
  moreover
  have "¬accepts (pre_star_exec A) c"
    using assms
    using accept_pre_star_exec_check_def calculation by auto
  ultimately
  show "c ∉ pre_star (lang A)"
    using accept_pre_star_exec_correct_False by auto
qed

theorem accept_pre_star_exec_correct_None:
  assumes "accept_pre_star_exec_check A c = None"
  shows "¬inits ⊆ LTS.srcs A"
  using assms unfolding accept_pre_star_exec_check_def by auto


subsection ‹Post* lemmas›

lemma lemma_3_3':
  assumes "pv ⇒⇧* p'w"
    and "(fst pv, snd pv) ∈ lang_ε A"
    and "saturation post_star_rules A A'"
  shows "accepts_ε A' (fst p'w, snd p'w)"
  using assms
proof (induct arbitrary: pv rule: rtranclp_induct)
  case base
  show ?case
    using assms post_star_lim'_incr_trans_star_ε
    by (auto simp: lang_ε_def accepts_ε_def)
next
  case (step p''u p'w)
  define p' where "p' = fst p'w"
  define w  where "w = snd p'w"
  define p'' where "p'' = fst p''u"
  define u  where "u = snd p''u"
  have p'w_def: "p'w = (p', w)"
    using p'_def w_def by auto
  have p''u_def: "p''u = (p'', u)"
    using p''_def u_def by auto

  then have "accepts_ε A' (p'', u)"
    using assms(2) p''_def step.hyps(3) step.prems(2) u_def by metis
  then have "∃q. q ∈ finals ∧ (Init p'', u, q) ∈ LTS_ε.trans_star_ε A'"
    by (auto simp: accepts_ε_def)
  then obtain q where q_p: "q ∈ finals ∧ (Init p'', u, q) ∈ LTS_ε.trans_star_ε A'"
    by metis
  then have "∃u_ε. q ∈ finals ∧ LTS_ε.ε_exp u_ε u ∧ (Init p'', u_ε, q) ∈ LTS.trans_star A'"
    using LTS_ε.trans_star_ε_iff_ε_exp_trans_star[of "Init p''" u q A'] by auto
  then obtain u_ε where II: "q ∈ finals" "LTS_ε.ε_exp u_ε u" "(Init p'', u_ε, q) ∈ LTS.trans_star A'"
    by blast
  have "∃γ u1 w1. u=γ#u1 ∧ w=lbl w1@u1 ∧ (p'', γ) ↪ (p', w1)"
    using p''u_def p'w_def step.hyps(2) step_relp_def2 by auto
  then obtain γ u1 w1 where III: "u=γ#u1" "w=lbl w1@u1" "(p'', γ) ↪ (p', w1)"
    by blast

  have p'_inits: "Init p' ∈ inits"
    unfolding inits_def by auto
  have p''_inits: "Init p'' ∈ inits"
    unfolding inits_def by auto

  have "∃γ_ε u1_ε. LTS_ε.ε_exp γ_ε [γ] ∧ LTS_ε.ε_exp u1_ε u1 ∧ (Init p'', γ_ε@u1_ε, q) ∈ LTS.trans_star A'"
  proof -
    have "∃γ_ε u1_ε. LTS_ε.ε_exp γ_ε [γ] ∧ LTS_ε.ε_exp u1_ε u1 ∧ u_ε = γ_ε @ u1_ε" 
      using LTS_ε.ε_exp_split'[of u_ε γ u1] II(2) III(1) by auto
    then obtain γ_ε u1_ε where "LTS_ε.ε_exp γ_ε [γ] ∧ LTS_ε.ε_exp u1_ε u1 ∧ u_ε = γ_ε @ u1_ε" 
      by auto
    then have "(Init p'', γ_ε@u1_ε , q) ∈ LTS.trans_star A'"
      using II(3) by auto
    then show ?thesis
      using ‹LTS_ε.ε_exp γ_ε [γ] ∧ LTS_ε.ε_exp u1_ε u1 ∧ u_ε = γ_ε @ u1_ε› by blast
  qed
  then obtain γ_ε u1_ε where 
    iii: "LTS_ε.ε_exp γ_ε [γ]" and 
    iv: "LTS_ε.ε_exp u1_ε u1" "(Init p'', γ_ε@u1_ε, q) ∈ LTS.trans_star A'"
    by blast
  then have VI: "∃q1. (Init p'', γ_ε, q1) ∈ LTS.trans_star A' ∧ (q1, u1_ε, q) ∈ LTS.trans_star A'"
    by (simp add: LTS.trans_star_split)
  then obtain q1 where VI: "(Init p'', γ_ε, q1) ∈ LTS.trans_star A'" "(q1, u1_ε, q) ∈ LTS.trans_star A'"
    by blast

  then have VI_2: "(Init p'', [γ], q1) ∈ LTS_ε.trans_star_ε A'" "(q1, u1, q) ∈ LTS_ε.trans_star_ε A'"
    by (meson LTS_ε.trans_star_ε_iff_ε_exp_trans_star iii VI(2) iv(1))+

  show ?case
  proof (cases w1)
    case pop
    then have r: "(p'', γ) ↪ (p', pop)"
      using III(3) by blast
    then have "(Init p', ε, q1) ∈ A'"
      using VI_2(1) add_trans_pop assms saturated_def saturation_def p'_inits by metis
    then have "(Init p', w, q) ∈ LTS_ε.trans_star_ε A'"
      using III(2) VI_2(2) pop LTS_ε.trans_star_ε.trans_star_ε_step_ε by fastforce
    then have "accepts_ε A' (p', w)"
      unfolding accepts_ε_def using II(1) by blast
    then show ?thesis
      using p'_def w_def by force
  next
    case (swap γ')
    then have r: "(p'', γ) ↪ (p', swap γ')"
      using III(3) by blast
    then have "(Init p', Some γ', q1) ∈ A'"
      by (metis VI_2(1) add_trans_swap assms(3) saturated_def saturation_def)
    have "(Init p', w, q) ∈ LTS_ε.trans_star_ε A'"
      using III(2) LTS_ε.trans_star_ε.trans_star_ε_step_γ VI_2(2) append_Cons append_self_conv2 
        lbl.simps(3) swap ‹(Init p', Some γ', q1) ∈ A'› by fastforce
    then have "accepts_ε A' (p', w)"
      unfolding accepts_ε_def
      using II(1) by blast
    then show ?thesis
      using p'_def w_def by force
  next
    case (push γ' γ'')
    then have r: "(p'', γ) ↪ (p', push γ' γ'')"
      using III(3) by blast
    from this VI_2 iii post_star_rules.intros(3)[OF this, of q1 A', OF VI_2(1)] 
    have "(Init p', Some γ', Isolated p' γ') ∈ A'"
      using assms(3) by (meson saturated_def saturation_def) 
    from this r VI_2 iii post_star_rules.intros(4)[OF r, of q1 A', OF VI_2(1)] 
    have "(Isolated p' γ', Some γ'', q1) ∈ A'"
      using assms(3) using saturated_def saturation_def by metis
    have "(Init p', [γ'], Isolated p' γ') ∈ LTS_ε.trans_star_ε A' ∧
          (Isolated p' γ', [γ''], q1) ∈ LTS_ε.trans_star_ε A' ∧
          (q1, u1, q) ∈ LTS_ε.trans_star_ε A'"
      by (metis LTS_ε.trans_star_ε.simps VI_2(2) ‹(Init p', Some γ', Isolated p' γ') ∈ A'› 
          ‹(Isolated p' γ', Some γ'', q1) ∈ A'›)
    have "(Init p', w, q) ∈ LTS_ε.trans_star_ε A'"
      using III(2) VI_2(2) ‹(Init p', Some γ', Isolated p' γ') ∈ A'› 
        ‹(Isolated p' γ', Some γ'', q1) ∈ A'› push LTS_ε.append_edge_edge_trans_star_ε by auto
    then have "accepts_ε A' (p', w)"
      unfolding accepts_ε_def
      using II(1) by blast
    then show ?thesis
      using p'_def w_def by force

  qed
qed

lemma lemma_3_3:
  assumes "(p,v) ⇒⇧* (p',w)"
  and "(p, v) ∈ lang_ε A"
  and "saturation post_star_rules A A'"
  shows "accepts_ε A' (p', w)"
  using assms lemma_3_3' by force

lemma init_only_hd:
  assumes "(ss, w) ∈ LTS.path_with_word A"
  assumes "inits ⊆ LTS.srcs A"
  assumes "count (transitions_of (ss, w)) t > 0"
  assumes "t = (Init p1, γ, q1)"
  shows "hd (transition_list (ss, w)) = t ∧ count (transitions_of (ss, w)) t = 1"
  using assms LTS.source_only_hd by (metis LTS.srcs_def2 inits_srcs_iff_Ctr_Loc_srcs)

lemma no_edge_to_Ctr_Loc_avoid_Ctr_Loc:
  assumes "(p, w, qq) ∈ LTS.trans_star Aiminus1"
  assumes "w ≠ []"
  assumes "inits ⊆ LTS.srcs Aiminus1"
  shows "qq ∉ inits"
  using assms LTS.no_end_in_source by (metis subset_iff)

lemma no_edge_to_Ctr_Loc_avoid_Ctr_Loc_ε:
  assumes "(p, [γ], qq) ∈ LTS_ε.trans_star_ε Aiminus1"
  assumes "inits ⊆ LTS.srcs Aiminus1"
  shows "qq ∉ inits"
  using assms LTS_ε.no_edge_to_source_ε by (metis subset_iff)

lemma no_edge_to_Ctr_Loc_post_star_rules':
  assumes "post_star_rules⇧*⇧* A Ai"
  assumes "∄q γ q'. (q, γ, Init q') ∈ A"
  shows "∄q γ q'. (q, γ, Init q') ∈ Ai"
using assms 
proof (induction rule: rtranclp_induct)
  case base
  then show ?case by auto
next
  case (step Aiminus1 Ai)
  then have ind: "∄q γ q'. (q, γ, Init q') ∈ Aiminus1"
    by auto
  from step(2) show ?case
  proof (cases rule: post_star_rules.cases)
    case (add_trans_pop p γ p' q)
    have "q ∉ inits"
      using ind no_edge_to_Ctr_Loc_avoid_Ctr_Loc_ε inits_srcs_iff_Ctr_Loc_srcs
      by (metis local.add_trans_pop(3))
    then have "∄qq. q = Init qq"
      by (simp add: inits_def is_Init_def)
    then show ?thesis
      using ind local.add_trans_pop(1) by auto
  next
    case (add_trans_swap p γ p' γ' q)
    have "q ∉ inits"
      using add_trans_swap ind no_edge_to_Ctr_Loc_avoid_Ctr_Loc_ε inits_srcs_iff_Ctr_Loc_srcs 
      by metis
    then have "∄qq. q = Init qq"
      by (simp add: inits_def is_Init_def)
    then show ?thesis
      using ind local.add_trans_swap(1) by auto
  next
    case (add_trans_push_1 p γ p' γ' γ'' q)
    have "q ∉ inits"
      using add_trans_push_1 ind no_edge_to_Ctr_Loc_avoid_Ctr_Loc_ε inits_srcs_iff_Ctr_Loc_srcs 
      by metis
    then have "∄qq. q = Init qq"
      by (simp add: inits_def is_Init_def)
    then show ?thesis
      using ind local.add_trans_push_1(1) by auto
  next
    case (add_trans_push_2 p γ p' γ' γ'' q)
    have "q ∉ inits"
      using add_trans_push_2 ind no_edge_to_Ctr_Loc_avoid_Ctr_Loc_ε inits_srcs_iff_Ctr_Loc_srcs 
      by metis
    then have "∄qq. q = Init qq"
      by (simp add: inits_def is_Init_def)
    then show ?thesis
      using ind local.add_trans_push_2(1) by auto
  qed
qed

lemma no_edge_to_Ctr_Loc_post_star_rules:
  assumes "post_star_rules⇧*⇧* A Ai"
  assumes "inits ⊆ LTS.srcs A"
  shows "inits ⊆ LTS.srcs Ai"
  using assms no_edge_to_Ctr_Loc_post_star_rules' inits_srcs_iff_Ctr_Loc_srcs by metis

lemma source_and_sink_isolated:
  assumes "N ⊆ LTS.srcs A"
  assumes "N ⊆ LTS.sinks A"
  shows "∀p γ q. (p, γ, q) ∈ A ⟶ p ∉ N ∧ q ∉ N"
  by (metis LTS.srcs_def2 LTS.sinks_def2 assms(1) assms(2) in_mono)

lemma post_star_rules_Isolated_source_invariant':
  assumes "post_star_rules⇧*⇧* A A'"
  assumes "isols ⊆ LTS.isolated A"
  assumes "(Init p', Some γ', Isolated p' γ') ∉ A'"
  shows "∄p γ. (p, γ, Isolated p' γ') ∈ A'"
  using assms 
proof (induction rule: rtranclp_induct)
  case base
  then show ?case 
    unfolding isols_def is_Isolated_def using LTS.isolated_no_edges by fastforce
next
  case (step Aiminus1 Ai)
  from step(2) show ?case
  proof (cases rule: post_star_rules.cases)
    case (add_trans_pop p''' γ'' p'' q)
    then have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
      using step.prems(2) by blast
    then have nin: "∄p γ. (p, γ, Isolated p' γ') ∈ Aiminus1"
      using local.add_trans_pop(1) step.IH step.prems(1,2) by fastforce
    then have "Isolated p' γ' ≠ q"
      using add_trans_pop(4) LTS_ε.trans_star_not_to_source_ε LTS.srcs_def2
      by (metis local.add_trans_pop(3) state.distinct(3))
    then have "∄p γ. (p, γ, Isolated p' γ') = (Init p'', ε, q)"
      by auto
    then show ?thesis
      using nin add_trans_pop(1) by auto
  next
    case (add_trans_swap p'''' γ'' p'' γ''' q)
    then have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
      using step.prems(2) by blast
    then have nin: "∄p γ. (p, γ, Isolated p' γ') ∈ Aiminus1"
      using local.add_trans_swap(1) step.IH step.prems(1,2) by fastforce
    then have "Isolated p' γ' ≠ q"
      using LTS.srcs_def2 
      by (metis state.distinct(4) LTS_ε.trans_star_not_to_source_ε local.add_trans_swap(3)) 
    then have "∄p γ. (p, γ, Isolated p' γ') = (Init p'', Some γ''', q)"
      by auto
    then show ?thesis
      using nin add_trans_swap(1) by auto
  next
    case (add_trans_push_1 p'''' γ'' p'' γ''' γ''''' q)
    then have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
      using step.prems(2) by blast
    then show ?thesis
      using add_trans_push_1(1) Un_iff state.inject(2) prod.inject singleton_iff step.IH 
        step.prems(1,2) by blast 
  next
    case (add_trans_push_2 p'''' γ'' p'' γ''' γ'''' q)
    have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
      using step.prems(2) .
    then have nin: "∄p γ. (p, γ, Isolated p' γ') ∈ Aiminus1"
      using local.add_trans_push_2(1) step.IH step.prems(1) by fastforce
    then have "Isolated p' γ' ≠ q"
      using LTS.srcs_def2 local.add_trans_push_2(3) 
      by (metis state.disc(1,3) LTS_ε.trans_star_not_to_source_ε)
    then have "∄p γ. (p, γ, Isolated p' γ') = (Init p'', ε, q)"
      by auto
    then show ?thesis
      using nin add_trans_push_2(1) by auto
  qed
qed

lemma post_star_rules_Isolated_source_invariant:
  assumes "post_star_rules⇧*⇧* A A'"
  assumes "isols ⊆ LTS.isolated A"
  assumes "(Init p', Some γ', Isolated p' γ') ∉ A'"
  shows "Isolated p' γ' ∈ LTS.srcs A'"
  by (meson LTS.srcs_def2 assms(1) assms(2) assms(3) post_star_rules_Isolated_source_invariant')

lemma post_star_rules_Isolated_sink_invariant':
  assumes "post_star_rules⇧*⇧* A A'"
  assumes "isols ⊆ LTS.isolated A"
  assumes "(Init p', Some γ', Isolated p' γ') ∉ A'"
  shows "∄p γ. (Isolated p' γ', γ, p) ∈ A'"
  using assms 
proof (induction rule: rtranclp_induct)
  case base
  then show ?case
    unfolding isols_def is_Isolated_def
    using LTS.isolated_no_edges by fastforce  
next
  case (step Aiminus1 Ai)
  from step(2) show ?case
  proof (cases rule: post_star_rules.cases)
    case (add_trans_pop p''' γ'' p'' q)
    then have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
      using step.prems(2) by blast
    then have nin: "∄p γ. (Isolated p' γ', γ, p) ∈ Aiminus1"
      using local.add_trans_pop(1) step.IH step.prems(1,2) by fastforce
    then have "Isolated p' γ' ≠ q"
      using add_trans_pop(4) 
        LTS_ε.trans_star_not_to_source_ε[of "Init p'''" "[γ'']" q Aiminus1 "Isolated p' γ'"]
        post_star_rules_Isolated_source_invariant local.add_trans_pop(1) step.hyps(1) step.prems(1,2)
        UnI1 local.add_trans_pop(3) by (metis (full_types) state.distinct(3))
    then have "∄p γ. (p, γ, Isolated p' γ') = (Init p'', ε, q)"
      by auto
    then show ?thesis
      using nin add_trans_pop(1) by auto
  next
    case (add_trans_swap p'''' γ'' p'' γ''' q)
    then have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
      using step.prems(2) by blast
    then have nin: "∄p γ. (Isolated p' γ', γ, p) ∈ Aiminus1"
      using local.add_trans_swap(1) step.IH step.prems(1,2) by fastforce
    then have "Isolated p' γ' ≠ q"
      using LTS_ε.trans_star_not_to_source_ε[of "Init p''''" "[γ'']" q Aiminus1] 
        local.add_trans_swap(3) post_star_rules_Isolated_source_invariant[of _ Aiminus1 p' γ'] UnCI 
        local.add_trans_swap(1) step.hyps(1) step.prems(1,2) state.simps(7) by metis
    then have "∄p γ. (p, γ, Isolated p' γ') = (Init p'', Some γ''', q)"
      by auto
    then show ?thesis
      using nin add_trans_swap(1) by auto
  next
    case (add_trans_push_1 p'''' γ'' p'' γ''' γ''''' q)
    then have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
      using step.prems(2) by blast
    then show ?thesis
      using add_trans_push_1(1) Un_iff state.inject prod.inject singleton_iff step.IH 
        step.prems(1,2) by blast 
  next
    case (add_trans_push_2 p'''' γ'' p'' γ''' γ'''' q)
    have "(Init p', Some γ', Isolated p' γ') ∉ Ai"
      using step.prems(2) by blast
    then have nin: "∄p γ. (Isolated p' γ', γ, p) ∈ Aiminus1"
      using local.add_trans_push_2(1) step.IH step.prems(1,2) by fastforce
    then have "Isolated p' γ' ≠ q"
      using state.disc(3) 
        LTS_ε.trans_star_not_to_source_ε[of "Init p''''" "[γ'']" q Aiminus1 "Isolated p' γ'"] 
        local.add_trans_push_2(3)
      using post_star_rules_Isolated_source_invariant[of _ Aiminus1 p' γ'] UnCI 
        local.add_trans_push_2(1) step.hyps(1) step.prems(1,2) state.disc(1) by metis
    then have "∄p γ. (Isolated p' γ', γ, p) = (Init p'', ε, q)"
      by auto
    then show ?thesis
      using nin add_trans_push_2(1)
      using local.add_trans_push_2 step.prems(2) by auto 
  qed
qed

lemma post_star_rules_Isolated_sink_invariant:
  assumes "post_star_rules⇧*⇧* A A'"
  assumes "isols ⊆ LTS.isolated A"
  assumes "(Init p', Some γ', Isolated p' γ') ∉ A'"
  shows "Isolated p' γ' ∈ LTS.sinks A'"
  by (meson LTS.sinks_def2 assms(1,2,3) post_star_rules_Isolated_sink_invariant')


― ‹Corresponds to Schwoon's lemma 3.4›
lemma rtranclp_post_star_rules_constains_successors_states:
  assumes "post_star_rules⇧*⇧* A A'"
  assumes "inits ⊆ LTS.srcs A"
  assumes "isols ⊆ LTS.isolated A"
  assumes "(Init p, w, ss, q) ∈ LTS.trans_star_states A'"
  shows "(¬is_Isolated q ⟶ (∃p' w'. (Init p', w', q) ∈ LTS_ε.trans_star_ε A ∧ (p',w') ⇒⇧* (p, LTS_ε.remove_ε w))) ∧
         (is_Isolated q ⟶ (the_Ctr_Loc q, [the_Label q]) ⇒⇧* (p, LTS_ε.remove_ε w))"
  using assms
proof (induction arbitrary: p q w ss rule: rtranclp_induct)
  case base
  {
    assume ctr_loc: "is_Init q ∨ is_Noninit q"
    then have "(Init p, LTS_ε.remove_ε w, q) ∈ LTS_ε.trans_star_ε A"
      using base LTS_ε.trans_star_states_trans_star_ε by metis
    then have "∃p' w'. (p', w', q) ∈ LTS_ε.trans_star_ε A"
      by auto
    then have ?case
      using ctr_loc ‹(Init p, LTS_ε.remove_ε w, q) ∈ LTS_ε.trans_star_ε A› by blast
  }
  moreover
  {
    assume "is_Isolated q"
    then have ?case
    proof (cases w)
      case Nil
      then have False using base
        using LTS.trans_star_empty LTS.trans_star_states_trans_star ‹is_Isolated q›
        by (metis state.disc(7))
      then show ?thesis
        by metis
    next
      case (Cons γ w_rest)
      then have "(Init p, γ#w_rest, ss, q) ∈ LTS.trans_star_states A"
        using base Cons by blast
      then have "∃s γ'. (s, γ', q) ∈ A"
        using LTS.trans_star_states_transition_relation by metis
      then have False
        using ‹is_Isolated q› isols_def base.prems(2) LTS.isolated_no_edges
        by (metis mem_Collect_eq subset_eq)
      then show ?thesis
        by auto
    qed
  }
  ultimately
  show ?case
   by (meson state.exhaust_disc)
next
  case (step Aiminus1 Ai)
  from step(2) have "∃p1 γ p2 w2 q1. Ai = Aiminus1 ∪ {(p1, γ, q1)} ∧ (p1, γ, q1) ∉ Aiminus1"
    by (cases rule: post_star_rules.cases) auto
  then obtain p1 γ q1 where p1_γ_p2_w2_q'_p:
    "Ai = Aiminus1 ∪ {(p1, γ, q1)}" 
    "(p1, γ, q1) ∉ Aiminus1"
    by auto

  define t where "t = (p1, γ, q1)"
  define j where "j = count (transitions_of' (Init p, w, ss, q)) t"

  note ss_p = step(6)

  from j_def ss_p show ?case
  proof (induction j arbitrary: p q w ss)
    case 0
    then have "(Init p, w, ss, q) ∈ LTS.trans_star_states Aiminus1"
      using count_zero_remove_path_with_word_trans_star_states p1_γ_p2_w2_q'_p(1) t_def
      by metis 
    then show ?case
      using step by auto
  next
    case (Suc j)
    from step(2) show ?case
    proof (cases rule: post_star_rules.cases)
      case (add_trans_pop p2 γ2 p1 q1) (* Note: p1 shadows p1 from above. q1 shadows q1 from above. *)
      note III = add_trans_pop(3)
      note VI = add_trans_pop(2)
      have t_def: "t = (Init p1, ε, q1)"
        using local.add_trans_pop(1) local.add_trans_pop p1_γ_p2_w2_q'_p(1) t_def by blast
      have init_Ai: "inits ⊆ LTS.srcs Ai"
        using step(1,2) step(4)
        using no_edge_to_Ctr_Loc_post_star_rules 
        using r_into_rtranclp by (metis)
      have t_hd_once: "hd (transition_list (ss, w)) = t ∧ count (transitions_of (ss, w)) t = 1"
      proof -
        have "(ss, w) ∈ LTS.path_with_word Ai"
          using Suc(3) LTS.trans_star_states_path_with_word by metis
        moreover 
        have "inits ⊆ LTS.srcs Ai"
          using init_Ai by auto
        moreover 
        have "0 < count (transitions_of (ss, w)) t"
          by (metis Suc.prems(1) transitions_of'.simps zero_less_Suc)
        moreover 
        have "t = (Init p1, ε, q1)"
          using t_def by auto
        moreover 
        have "Init p1 ∈ inits"
          by (simp add: inits_def)
        ultimately
        show "hd (transition_list (ss, w)) = t ∧ count (transitions_of (ss, w)) t = 1"
          using init_only_hd[of ss w Ai t p1 ε q1] by auto
      qed

      have "transition_list (ss, w) ≠ []"
        by (metis LTS.trans_star_states_path_with_word LTS.path_with_word.simps Suc.prems(1)
            Suc.prems(2) count_empty less_not_refl2 list.distinct(1) transition_list.simps(1) 
            transitions_of'.simps transitions_of.simps(2) zero_less_Suc)
      then have ss_w_split: "([Init p1,q1], [ε]) @´ (tl ss,  tl w) = (ss, w)"
        using t_hd_once t_def hd_transition_list_append_path_with_word by metis
      then have ss_w_split': "(Init p1, [ε], [Init p1,q1], q1) @@´ (q1, tl w, tl ss, q) = (Init p1, w, ss, q)"
        by auto
      have VII: "p = p1"
      proof -
        have "(Init p, w, ss, q) ∈ LTS.trans_star_states Ai"
          using Suc.prems(2) by blast
        moreover
        have "t = hd (transition_list' (Init p, w, ss, q))"
          using ‹hd (transition_list (ss, w)) = t ∧ count (transitions_of (ss, w)) t = 1› 
          by fastforce
        moreover
        have "transition_list' (Init p, w, ss, q) ≠ []"
          by (simp add: ‹transition_list (ss, w) ≠ []›)
        moreover
        have "t = (Init p1, ε, q1)"
          using t_def by auto
        ultimately
        show "p = p1"
          using LTS.hd_is_hd by fastforce
      qed
      have "j=0"
        using Suc(2) ‹hd (transition_list (ss, w)) = t ∧ count (transitions_of (ss, w)) t = 1› 
        by force
      have "(Init p1, [ε], [Init p1, q1], q1) ∈ LTS.trans_star_states Ai"
      proof -
        have "(Init p1, ε, q1) ∈ Ai"
          using local.add_trans_pop(1) by auto
        moreover
        have "(Init p1, ε, q1) ∉ Aiminus1"
          by (simp add: local.add_trans_pop)
        ultimately
        show "(Init p1, [ε], [Init p1, q1], q1) ∈ LTS.trans_star_states Ai"
          by (meson LTS.trans_star_states.trans_star_states_refl 
              LTS.trans_star_states.trans_star_states_step)
      qed
      have "(q1, tl w, tl ss, q) ∈ LTS.trans_star_states Aiminus1"
      proof -
        from Suc(3) have "(ss, w) ∈ LTS.path_with_word Ai"
          by (meson LTS.trans_star_states_path_with_word)
        then have tl_ss_w_Ai: "(tl ss, tl w) ∈ LTS.path_with_word Ai"
          by (metis LTS.path_with_word.simps ‹transition_list (ss, w) ≠ []› list.sel(3) 
              transition_list.simps(2))
        from t_hd_once have zero_p1_ε_q1: "0 = count (transitions_of (tl ss, tl w)) (Init p1, ε, q1)"
          using count_append_path_with_word_γ[of "[hd ss]" "[]" "tl ss" "hd w" "tl w" "Init p1" ε q1, simplified]
            ‹(Init p1, [ε], [Init p1, q1], q1) ∈ LTS.trans_star_states Ai› 
            ‹transition_list (ss, w) ≠ []› Suc.prems(2) VII 
            LTS.transition_list_Cons[of "Init p" w ss q Ai ε q1] by (auto simp: t_def)
        have Ai_Aiminus1: "Ai = Aiminus1 ∪ {(Init p1, ε, q1)}"
          using local.add_trans_pop(1) by auto
        from t_hd_once tl_ss_w_Ai zero_p1_ε_q1 Ai_Aiminus1 
          count_zero_remove_path_with_word[OF tl_ss_w_Ai, of "Init p1" ε q1 Aiminus1] 
        have "(tl ss, tl w) ∈ LTS.path_with_word Aiminus1"
          by auto
        moreover
        have "hd (tl ss) = q1"
          using Suc.prems(2) VII ‹transition_list (ss, w) ≠ []› t_def 
            LTS.transition_list_Cons t_hd_once by fastforce
        moreover
        have "last ss = q"
          by (metis LTS.trans_star_states_last Suc.prems(2))
        ultimately
        show "(q1, tl w, tl ss, q) ∈ LTS.trans_star_states Aiminus1"
          by (metis (no_types, lifting) LTS.trans_star_states_path_with_word 
              LTS.path_with_word_trans_star_states LTS.path_with_word_not_empty Suc.prems(2) 
              last_ConsR list.collaps