Theory LTS

(*  Title:      JinjaThreads/Framework/LTS.thy
    Author:     Andreas Lochbihler
*)

section ‹Labelled transition systems›

theory LTS
imports
  "../Basic/Auxiliary"
  Coinductive.TLList
begin

unbundle no floor_ceiling_syntax

lemma rel_option_mono:
  "⟦ rel_option R x y; ⋀x y. R x y ⟹ R' x y ⟧ ⟹ rel_option R' x y"
by(cases x)(case_tac [!] y, auto)

lemma nth_concat_conv:
  "n < length (concat xss) 
   ⟹ ∃m n'. concat xss ! n = (xss ! m) ! n' ∧ n' < length (xss ! m) ∧ 
             m < length xss ∧ n = (∑i<m. length (xss ! i)) + n'"
using lnth_lconcat_conv[of n "llist_of (map llist_of xss)"]
  sum_comp_morphism[where h = enat and g = "λi. length (xss ! i)"]
by(clarsimp simp add: lconcat_llist_of zero_enat_def[symmetric]) blast


definition flip :: "('a ⇒ 'b ⇒ 'c) ⇒ 'b ⇒ 'a ⇒ 'c"
where "flip f = (λb a. f a b)"

text ‹Create a dynamic list ‹flip_simps› of theorems for flip›
ML ‹
structure FlipSimpRules = Named_Thms
(
  val name = @{binding flip_simps}
  val description = "Simplification rules for flip in bisimulations"
)
›
setup ‹FlipSimpRules.setup›

lemma flip_conv [flip_simps]: "flip f b a = f a b"
by(simp add: flip_def)

lemma flip_flip [flip_simps, simp]: "flip (flip f) = f"
by(simp add: flip_def)

lemma list_all2_flip [flip_simps]: "list_all2 (flip P) xs ys = list_all2 P ys xs"
unfolding flip_def list_all2_conv_all_nth by auto

lemma llist_all2_flip [flip_simps]: "llist_all2 (flip P) xs ys = llist_all2 P ys xs"
unfolding flip_def llist_all2_conv_all_lnth by auto

lemma rtranclp_flipD:
  assumes "(flip r)^** x y"
  shows "r^** y x" 
using assms
by(induct rule: rtranclp_induct)(auto intro: rtranclp.rtrancl_into_rtrancl simp add: flip_conv)

lemma rtranclp_flip [flip_simps]:
  "(flip r)^** = flip r^**"
by(auto intro!: ext simp add: flip_conv intro: rtranclp_flipD)

lemma rel_prod_flip [flip_simps]:
  "rel_prod (flip R) (flip S) = flip (rel_prod R S)"
by(auto intro!: ext simp add: flip_def)

lemma rel_option_flip [flip_simps]:
  "rel_option (flip R) = flip (rel_option R)"
by(simp add: fun_eq_iff rel_option_iff flip_def)

lemma tllist_all2_flip [flip_simps]:
  "tllist_all2 (flip P) (flip Q) xs ys ⟷ tllist_all2 P Q ys xs"
proof
  assume "tllist_all2 (flip P) (flip Q) xs ys"
  thus "tllist_all2 P Q ys xs"
    by(coinduct rule: tllist_all2_coinduct)(auto dest: tllist_all2_is_TNilD tllist_all2_tfinite2_terminalD tllist_all2_thdD intro: tllist_all2_ttlI simp add: flip_def)
next
  assume "tllist_all2 P Q ys xs"
  thus "tllist_all2 (flip P) (flip Q) xs ys"
    by(coinduct rule: tllist_all2_coinduct)(auto dest: tllist_all2_is_TNilD tllist_all2_tfinite2_terminalD tllist_all2_thdD intro: tllist_all2_ttlI simp add: flip_def)
qed

subsection ‹Labelled transition systems›

type_synonym ('a, 'b) trsys = "'a ⇒ 'b ⇒ 'a ⇒ bool"

locale trsys = 
  fixes trsys :: "('s, 'tl) trsys" (‹_/ -_→/ _› [50, 0, 50] 60)
begin

abbreviation Trsys :: "('s, 'tl list) trsys" (‹_/ -_→*/ _› [50,0,50] 60)
where "⋀tl. s -tl→* s' ≡ rtrancl3p trsys s tl s'"

coinductive inf_step :: "'s ⇒ 'tl llist ⇒ bool" (‹_ -_→* ∞› [50, 0] 80)
where inf_stepI: "⟦ trsys a b a'; a' -bs→* ∞ ⟧ ⟹ a -LCons b bs→* ∞"

coinductive inf_step_table :: "'s ⇒ ('s × 'tl × 's) llist ⇒ bool" (‹_ -_→*t ∞› [50, 0] 80)
where 
  inf_step_tableI:
  "⋀tl. ⟦ trsys s tl s'; s' -stls→*t ∞ ⟧ 
  ⟹ s -LCons (s, tl, s') stls→*t ∞"

definition inf_step2inf_step_table :: "'s ⇒ 'tl llist ⇒ ('s × 'tl × 's) llist"
where
  "inf_step2inf_step_table s tls =
   unfold_llist
     (λ(s, tls). lnull tls)
     (λ(s, tls). (s, lhd tls, SOME s'. trsys s (lhd tls) s' ∧ s' -ltl tls→* ∞)) 
     (λ(s, tls). (SOME s'. trsys s (lhd tls) s' ∧ s' -ltl tls→* ∞, ltl tls))
     (s, tls)"

coinductive Rtrancl3p :: "'s ⇒ ('tl, 's) tllist ⇒ bool"
where 
  Rtrancl3p_stop: "(⋀tl s'. ¬ s -tl→ s') ⟹  Rtrancl3p s (TNil s)"
| Rtrancl3p_into_Rtrancl3p: "⋀tl. ⟦ s -tl→ s'; Rtrancl3p s' tlss ⟧ ⟹ Rtrancl3p s (TCons tl tlss)"
  
inductive_simps Rtrancl3p_simps:
  "Rtrancl3p s (TNil s')"
  "Rtrancl3p s (TCons tl' tlss)"

inductive_cases Rtrancl3p_cases:
  "Rtrancl3p s (TNil s')"
  "Rtrancl3p s (TCons tl' tlss)"

coinductive Runs :: "'s ⇒ 'tl llist ⇒ bool"
where
  Stuck: "(⋀tl s'. ¬ s -tl→ s') ⟹ Runs s LNil"
| Step: "⋀tl. ⟦ s -tl→ s'; Runs s' tls ⟧ ⟹ Runs s (LCons tl tls)"

coinductive Runs_table :: "'s ⇒ ('s × 'tl × 's) llist ⇒ bool"
where
  Stuck: "(⋀tl s'. ¬ s -tl→ s') ⟹ Runs_table s LNil"
| Step: "⋀tl. ⟦ s -tl→ s'; Runs_table s' stlss ⟧ ⟹ Runs_table s (LCons (s, tl, s') stlss)"

inductive_simps Runs_table_simps:
  "Runs_table s LNil"
  "Runs_table s (LCons stls stlss)"

lemma inf_step_not_finite_llist:
  assumes r: "s -bs→* ∞"
  shows "¬ lfinite bs"
proof
  assume "lfinite bs" thus False using r
    by(induct arbitrary: s rule: lfinite.induct)(auto elim: inf_step.cases)
qed

lemma inf_step2inf_step_table_LNil [simp]: "inf_step2inf_step_table s LNil = LNil"
by(simp add: inf_step2inf_step_table_def)

lemma inf_step2inf_step_table_LCons [simp]:
  fixes tl shows
  "inf_step2inf_step_table s (LCons tl tls) =
   LCons (s, tl, SOME s'. trsys s tl s' ∧ s' -tls→* ∞) 
         (inf_step2inf_step_table (SOME s'. trsys s tl s' ∧ s' -tls→* ∞) tls)"
by(simp add: inf_step2inf_step_table_def)

lemma lnull_inf_step2inf_step_table [simp]: 
  "lnull (inf_step2inf_step_table s tls) ⟷ lnull tls"
by(simp add: inf_step2inf_step_table_def)

lemma inf_step2inf_step_table_eq_LNil: 
  "inf_step2inf_step_table s tls = LNil ⟷ tls = LNil"
using lnull_inf_step2inf_step_table unfolding lnull_def .

lemma lhd_inf_step2inf_step_table [simp]:
  "¬ lnull tls
  ⟹ lhd (inf_step2inf_step_table s tls) =
      (s, lhd tls, SOME s'. trsys s (lhd tls) s' ∧ s' -ltl tls→* ∞)"
by(simp add: inf_step2inf_step_table_def)

lemma ltl_inf_step2inf_step_table [simp]:
  "ltl (inf_step2inf_step_table s tls) =
   inf_step2inf_step_table (SOME s'. trsys s (lhd tls) s' ∧ s' -ltl tls→* ∞) (ltl tls)"
by(cases tls) simp_all

lemma lmap_inf_step2inf_step_table: "lmap (fst ∘ snd) (inf_step2inf_step_table s tls) = tls"
by(coinduction arbitrary: s tls) auto

lemma inf_step_imp_inf_step_table:
  assumes "s -tls→* ∞"
  shows "∃stls. s -stls→*t ∞ ∧ tls = lmap (fst ∘ snd) stls"
proof -
  from assms have "s -inf_step2inf_step_table s tls→*t ∞"
  proof(coinduction arbitrary: s tls)
    case (inf_step_table s tls)
    thus ?case
    proof cases
      case (inf_stepI tl s' tls')
      let ?s' = "SOME s'. trsys s tl s' ∧ s' -tls'→* ∞"
      have "trsys s tl ?s' ∧ ?s' -tls'→* ∞" by(rule someI)(blast intro: inf_stepI)
      thus ?thesis using ‹tls = LCons tl tls'› by auto
    qed
  qed
  moreover have "tls = lmap (fst ∘ snd) (inf_step2inf_step_table s tls)"
    by(simp only: lmap_inf_step2inf_step_table)
  ultimately show ?thesis by blast
qed

lemma inf_step_table_imp_inf_step:
  "s-stls→*t ∞ ⟹s -lmap (fst ∘ snd) stls→* ∞"
proof(coinduction arbitrary: s stls rule: inf_step.coinduct)
  case (inf_step s tls)
  thus ?case by cases auto
qed

lemma Runs_table_into_Runs:
  "Runs_table s stlss ⟹ Runs s (lmap (λ(s, tl, s'). tl) stlss)"
proof(coinduction arbitrary: s stlss)
  case (Runs s tls)
  thus ?case by (cases)auto
qed

lemma Runs_into_Runs_table:
  assumes "Runs s tls"
  obtains stlss
  where "tls = lmap (λ(s, tl, s'). tl) stlss"
  and "Runs_table s stlss"
proof -
  define stlss where "stlss s tls = unfold_llist
    (λ(s, tls). lnull tls)
    (λ(s, tls). (s, lhd tls, SOME s'. s -lhd tls→ s' ∧ Runs s' (ltl tls)))
    (λ(s, tls). (SOME s'. s -lhd tls→ s' ∧ Runs s' (ltl tls), ltl tls))
    (s, tls)"
    for s tls
  have [simp]:
    "⋀s. stlss s LNil = LNil"
    "⋀s tl tls. stlss s (LCons tl tls) = LCons (s, tl, SOME s'. s -tl→ s' ∧ Runs s' tls) (stlss (SOME s'. s -tl→ s' ∧ Runs s' tls) tls)"
    "⋀s tls. lnull (stlss s tls) ⟷ lnull tls"
    "⋀s tls. ¬ lnull tls ⟹ lhd (stlss s tls) = (s, lhd tls, SOME s'. s -lhd tls→ s' ∧ Runs s' (ltl tls))"
    "⋀s tls. ¬ lnull tls ⟹ ltl (stlss s tls) = stlss (SOME s'. s -lhd tls→ s' ∧ Runs s' (ltl tls)) (ltl tls)"
    by(simp_all add: stlss_def)
  
  from assms have "tls = lmap (λ(s, tl, s'). tl) (stlss s tls)"
  proof(coinduction arbitrary: s tls)
    case Eq_llist
    thus ?case by cases(auto 4 3 intro: someI2)
  qed
  moreover
  from assms have "Runs_table s (stlss s tls)"
  proof(coinduction arbitrary: s tls)
    case (Runs_table s stlss')
    thus ?case
    proof(cases)
      case (Step s' tls' tl)
      let ?P = "λs'. s -tl→ s' ∧ Runs s' tls'"
      from ‹s -tl→ s'› ‹Runs s' tls'› have "?P s'" ..
      hence "?P (Eps ?P)" by(rule someI)
      with Step have ?Step by auto
      thus ?thesis ..
    qed simp
  qed
  ultimately show ?thesis by(rule that)
qed

lemma Runs_lappendE:
  assumes "Runs σ (lappend tls tls')"
  and "lfinite tls"
  obtains σ' where "σ -list_of tls→* σ'"
  and "Runs σ' tls'"
proof(atomize_elim)
  from ‹lfinite tls› ‹Runs σ (lappend tls tls')›
  show "∃σ'. σ -list_of tls→* σ' ∧ Runs σ' tls'"
  proof(induct arbitrary: σ)
    case lfinite_LNil thus ?case by(auto)
  next
    case (lfinite_LConsI tls tl)
    from ‹Runs σ (lappend (LCons tl tls) tls')›
    show ?case unfolding lappend_code
    proof(cases)
      case (Step σ')
      from ‹Runs σ' (lappend tls tls') ⟹ ∃σ''. σ' -list_of tls→* σ'' ∧ Runs σ'' tls'› ‹Runs σ' (lappend tls tls')›
      obtain σ'' where "σ' -list_of tls→* σ''" "Runs σ'' tls'" by blast
      from ‹σ -tl→ σ'› ‹σ' -list_of tls→* σ''›
      have "σ -tl # list_of tls→* σ''" by(rule rtrancl3p_step_converse)
      with ‹lfinite tls› have "σ -list_of (LCons tl tls)→* σ''" by(simp)
      with ‹Runs σ'' tls'› show ?thesis by blast
    qed
  qed
qed

lemma Trsys_into_Runs:
  assumes "s -tls→* s'"
  and "Runs s' tls'"
  shows "Runs s (lappend (llist_of tls) tls')"
using assms
by(induct rule: rtrancl3p_converse_induct)(auto intro: Runs.Step)

lemma rtrancl3p_into_Rtrancl3p:
  "⟦ rtrancl3p trsys a bs a'; ⋀b a''. ¬ a' -b→ a'' ⟧ ⟹ Rtrancl3p a (tllist_of_llist a' (llist_of bs))"
  by(induct rule: rtrancl3p_converse_induct)(auto intro: Rtrancl3p.intros)
    
lemma Rtrancl3p_into_Runs:
  "Rtrancl3p s tlss ⟹ Runs s (llist_of_tllist tlss)"
by(coinduction arbitrary: s tlss rule: Runs.coinduct)(auto elim: Rtrancl3p.cases)

lemma Runs_into_Rtrancl3p:
  assumes "Runs s tls"
  obtains tlss where "tls = llist_of_tllist tlss" "Rtrancl3p s tlss"
proof
  let ?Q = "λs tls s'. s -lhd tls→ s' ∧ Runs s' (ltl tls)"
  define tlss where "tlss = corec_tllist 
    (λ(s, tls). lnull tls) (λ(s, tls). s)
    (λ(s, tls). lhd tls)
    (λ_. False) undefined (λ(s, tls). (SOME s'. ?Q s tls s', ltl tls))"
  have [simp]:
    "tlss (s, LNil) = TNil s"
    "tlss (s, LCons tl tls) = TCons tl (tlss (SOME s'. ?Q s (LCons tl tls) s', tls))"
    for s tl tls by(auto simp add: tlss_def intro: tllist.expand)

  show "tls = llist_of_tllist (tlss (s, tls))" using assms
    by(coinduction arbitrary: s tls)(erule Runs.cases; fastforce intro: someI2)
      
  show "Rtrancl3p s (tlss (s, tls))" using assms
    by(coinduction arbitrary: s tls)(erule Runs.cases; simp; iprover intro: someI2[where Q="trsys _ _"] someI2[where Q="λs'. Runs s' _"])
qed

lemma fixes tl
  assumes "Rtrancl3p s tlss" "tfinite tlss"
  shows Rtrancl3p_into_Trsys: "Trsys s (list_of (llist_of_tllist tlss)) (terminal tlss)"
    and terminal_Rtrancl3p_final: "¬ terminal tlss -tl→ s'"
using assms(2,1) by(induction arbitrary: s rule: tfinite_induct)(auto simp add: Rtrancl3p_simps intro: rtrancl3p_step_converse)

end
  
subsection ‹Labelled transition systems with internal actions›

locale τtrsys = trsys +
  constrains trsys :: "('s, 'tl) trsys"
  fixes τmove :: "('s, 'tl) trsys"
begin

inductive silent_move :: "'s ⇒ 's ⇒ bool" (‹_ -τ→ _› [50, 50] 60)
where [intro]: "!!tl. ⟦ trsys s tl s'; τmove s tl s' ⟧ ⟹ s -τ→ s'"

declare silent_move.cases [elim]

lemma silent_move_iff: "silent_move = (λs s'. (∃tl. trsys s tl s' ∧ τmove s tl s'))"
by(auto simp add: fun_eq_iff)

abbreviation silent_moves :: "'s ⇒ 's ⇒ bool" (‹_ -τ→* _› [50, 50] 60)
where "silent_moves == silent_move^**"

abbreviation silent_movet :: "'s ⇒ 's ⇒ bool" (‹_ -τ→+ _› [50, 50] 60)
where "silent_movet == silent_move^++"

coinductive τdiverge :: "'s ⇒ bool" (‹_ -τ→ ∞› [50] 60)
where
  τdivergeI: "⟦ s -τ→ s'; s' -τ→ ∞ ⟧ ⟹ s -τ→ ∞"

coinductive τinf_step :: "'s ⇒ 'tl llist ⇒ bool" (‹_ -τ-_→* ∞› [50, 0] 60)
where
  τinf_step_Cons: "⋀tl. ⟦ s -τ→* s'; s' -tl→ s''; ¬ τmove s' tl s''; s'' -τ-tls→* ∞ ⟧ ⟹ s -τ-LCons tl tls→* ∞"
| τinf_step_Nil: "s -τ→ ∞ ⟹ s -τ-LNil→* ∞"

coinductive τinf_step_table :: "'s ⇒ ('s × 's × 'tl × 's) llist ⇒ bool" (‹_ -τ-_→*t ∞› [50, 0] 80)
where
  τinf_step_table_Cons:
  "⋀tl. ⟦ s -τ→* s'; s' -tl→ s''; ¬ τmove s' tl s''; s'' -τ-tls→*t ∞ ⟧ ⟹ s -τ-LCons (s, s', tl, s'') tls→*t ∞"

| τinf_step_table_Nil:
  "s -τ→ ∞ ⟹ s -τ-LNil→*t ∞"

definition τinf_step2τinf_step_table :: "'s ⇒ 'tl llist ⇒ ('s × 's × 'tl × 's) llist"
where
  "τinf_step2τinf_step_table s tls =
   unfold_llist
     (λ(s, tls). lnull tls)
     (λ(s, tls). let (s', s'') = SOME (s', s''). s -τ→* s' ∧ s' -lhd tls→ s'' ∧ ¬ τmove s' (lhd tls) s'' ∧ s'' -τ-ltl tls→* ∞
        in (s, s', lhd tls, s''))
     (λ(s, tls). let (s', s'') = SOME (s', s''). s -τ→* s' ∧ s' -lhd tls→ s'' ∧ ¬ τmove s' (lhd tls) s'' ∧ s'' -τ-ltl tls→* ∞
        in (s'', ltl tls))
     (s, tls)"

definition silent_move_from :: "'s ⇒ 's ⇒ 's ⇒ bool"
where "silent_move_from s0 s1 s2 ⟷ silent_moves s0 s1 ∧ silent_move s1 s2"

inductive τrtrancl3p :: "'s ⇒ 'tl list ⇒ 's ⇒ bool" (‹_ -τ-_→* _› [50, 0, 50] 60)
where
  τrtrancl3p_refl: "τrtrancl3p s [] s"
| τrtrancl3p_step: "⋀tl. ⟦ s -tl→ s'; ¬ τmove s tl s'; τrtrancl3p s' tls s'' ⟧ ⟹ τrtrancl3p s (tl # tls) s''"
| τrtrancl3p_τstep: "⋀tl. ⟦ s -tl→ s'; τmove s tl s'; τrtrancl3p s' tls s'' ⟧ ⟹ τrtrancl3p s tls s''"

coinductive τRuns :: "'s ⇒ ('tl, 's option) tllist ⇒ bool" (‹_ ⇓ _› [50, 50] 51)
where
  Terminate: "⟦ s -τ→* s'; ⋀tl s''. ¬ s' -tl→ s'' ⟧ ⟹ s ⇓ TNil ⌊s'⌋" 
| Diverge: "s -τ→ ∞ ⟹ s ⇓ TNil None"
| Proceed: "⋀tl. ⟦ s -τ→* s'; s' -tl→ s''; ¬ τmove s' tl s''; s'' ⇓ tls ⟧ ⟹ s ⇓ TCons tl tls"

inductive_simps τRuns_simps:
  "s ⇓ TNil (Some s')"
  "s ⇓ TNil None"
  "s ⇓ TCons tl' tls"

coinductive τRuns_table :: "'s ⇒ ('tl × 's, 's option) tllist ⇒ bool"
where 
  Terminate: "⟦ s -τ→* s'; ⋀tl s''. ¬ s' -tl→ s'' ⟧ ⟹ τRuns_table s (TNil ⌊s'⌋)"
| Diverge: "s -τ→ ∞ ⟹ τRuns_table s (TNil None)"
| Proceed:
  "⋀tl. ⟦ s -τ→* s'; s' -tl→ s''; ¬ τmove s' tl s''; τRuns_table s'' tls ⟧ 
  ⟹ τRuns_table s (TCons (tl, s'') tls)"

definition silent_move2 :: "'s ⇒ 'tl ⇒ 's ⇒ bool"
where "⋀tl. silent_move2 s tl s' ⟷ s -tl→ s' ∧ τmove s tl s'"

abbreviation silent_moves2 :: "'s ⇒ 'tl list ⇒ 's ⇒ bool"
where "silent_moves2 ≡ rtrancl3p silent_move2"

coinductive τRuns_table2 :: "'s ⇒ ('tl list × 's × 'tl × 's, ('tl list × 's) + 'tl llist) tllist ⇒ bool"
where 
  Terminate: "⟦ silent_moves2 s tls s'; ⋀tl s''. ¬ s' -tl→ s'' ⟧ ⟹ τRuns_table2 s (TNil (Inl (tls, s')))"
| Diverge: "trsys.inf_step silent_move2 s tls ⟹ τRuns_table2 s (TNil (Inr tls))"
| Proceed:
  "⋀tl. ⟦ silent_moves2 s tls s'; s' -tl→ s''; ¬ τmove s' tl s''; τRuns_table2 s'' tlsstlss ⟧ 
  ⟹ τRuns_table2 s (TCons (tls, s', tl, s'') tlsstlss)"

inductive_simps τRuns_table2_simps:
  "τRuns_table2 s (TNil tlss)"
  "τRuns_table2 s (TCons tlsstls tlsstlss)"

lemma inf_step_table_all_τ_into_τdiverge:
  "⟦ s -stls→*t ∞; ∀(s, tl, s') ∈ lset stls. τmove s tl s' ⟧ ⟹ s -τ→ ∞"
proof(coinduction arbitrary: s stls)
  case (τdiverge s)
  thus ?case by cases (auto simp add: silent_move_iff, blast)
qed

lemma inf_step_table_lappend_llist_ofD:
  "s -lappend (llist_of stls) (LCons (x, tl', x') xs)→*t ∞
  ⟹ (s -map (fst ∘ snd) stls→* x) ∧ (x -LCons (x, tl', x') xs→*t ∞)"
proof(induct stls arbitrary: s)
  case Nil thus ?case by(auto elim: inf_step_table.cases intro: inf_step_table.intros rtrancl3p_refl)
next
  case (Cons st stls)
  note IH = ‹⋀s. s -lappend (llist_of stls) (LCons (x, tl', x') xs)→*t ∞ ⟹
                 s -map (fst ∘ snd) stls→* x ∧ x -LCons (x, tl', x') xs→*t ∞›
  from ‹s -lappend (llist_of (st # stls)) (LCons (x, tl', x') xs)→*t ∞›
  show ?case
  proof cases
    case (inf_step_tableI s' stls' tl)
    hence [simp]: "st = (s, tl, s')" "stls' = lappend (llist_of stls) (LCons (x, tl', x') xs)"
      and "s -tl→ s'" "s' -lappend (llist_of stls) (LCons (x, tl', x') xs)→*t ∞" by simp_all
    from IH[OF ‹s' -lappend (llist_of stls) (LCons (x, tl', x') xs)→*t ∞›]
    have "s' -map (fst ∘ snd) stls→* x" "x -LCons (x, tl', x') xs→*t ∞" by auto
    with ‹s -tl→ s'› show ?thesis by(auto simp add: o_def intro: rtrancl3p_step_converse)
  qed
qed

lemma inf_step_table_lappend_llist_of_τ_into_τmoves:
  assumes "lfinite stls"
  shows "⟦ s -lappend stls (LCons (x, tl' x') xs)→*t ∞; ∀(s, tl, s')∈lset stls. τmove s tl s' ⟧ ⟹ s -τ→* x"
using assms
proof(induct arbitrary: s rule: lfinite.induct)
  case lfinite_LNil thus ?case by(auto elim: inf_step_table.cases)
next
  case (lfinite_LConsI stls st)
  note IH = ‹⋀s. ⟦s -lappend stls (LCons (x, tl' x') xs)→*t ∞; ∀(s, tl, s')∈lset stls. τmove s tl s' ⟧ ⟹ s -τ→* x›
  obtain s1 tl1 s1' where [simp]: "st = (s1, tl1, s1')" by(cases st)
  from ‹s -lappend (LCons st stls) (LCons (x, tl' x') xs)→*t ∞›
  show ?case
  proof cases
    case (inf_step_tableI X' STLS TL)
    hence [simp]: "s1 = s" "TL = tl1" "X' = s1'" "STLS = lappend stls (LCons (x, tl' x') xs)"
      and "s -tl1→ s1'" and "s1' -lappend stls (LCons (x, tl' x') xs)→*t ∞" by simp_all
    from ‹∀(s, tl, s')∈lset (LCons st stls). τmove s tl s'› have "τmove s tl1 s1'" by simp
    moreover
    from IH[OF ‹s1' -lappend stls (LCons (x, tl' x') xs)→*t ∞›] ‹∀(s, tl, s')∈lset (LCons st stls). τmove s tl s'›
    have "s1' -τ→* x" by simp
    ultimately show ?thesis using ‹s -tl1→ s1'› by(auto intro: converse_rtranclp_into_rtranclp)
  qed
qed


lemma inf_step_table_into_τinf_step:
  "s -stls→*t ∞ ⟹ s -τ-lmap (fst ∘ snd) (lfilter (λ(s, tl, s'). ¬ τmove s tl s') stls)→* ∞"
proof(coinduction arbitrary: s stls)
  case (τinf_step s stls)
  let ?P = "λ(s, tl, s'). ¬ τmove s tl s'"
  show ?case
  proof(cases "lfilter ?P stls")
    case LNil
    with τinf_step have ?τinf_step_Nil
      by(auto intro: inf_step_table_all_τ_into_τdiverge simp add: lfilter_eq_LNil)
    thus ?thesis ..
  next
    case (LCons stls' xs)
    obtain x tl x' where "stls' = (x, tl, x')" by(cases stls')
    with LCons have stls: "lfilter ?P stls = LCons (x, tl, x') xs" by simp
    from lfilter_eq_LConsD[OF this] obtain stls1 stls2
      where stls1: "stls = lappend stls1 (LCons (x, tl, x') stls2)"
      and "lfinite stls1"
      and τs: "∀(s, tl, s')∈lset stls1. τmove s tl s'"
      and nτ: "¬ τmove x tl x'" and xs: "xs = lfilter ?P stls2" by blast
    from ‹lfinite stls1› τinf_step τs have "s -τ→* x" unfolding stls1
      by(rule inf_step_table_lappend_llist_of_τ_into_τmoves)
    moreover from ‹lfinite stls1› have "llist_of (list_of stls1) = stls1" by(simp add: llist_of_list_of)
    with τinf_step stls1 have "s -lappend (llist_of (list_of stls1)) (LCons (x, tl, x') stls2)→*t ∞" by simp
    from inf_step_table_lappend_llist_ofD[OF this]
    have "x -LCons (x, tl, x') stls2→*t ∞" ..
    hence "x -tl→ x'" "x' -stls2→*t ∞" by(auto elim: inf_step_table.cases)
    ultimately have ?τinf_step_Cons using xs nτ by(auto simp add: stls o_def)
    thus ?thesis ..
  qed
qed

lemma inf_step_into_τinf_step:
  assumes "s -tls→* ∞"
  shows "∃A. s -τ-lnths tls A→* ∞"
proof -
  from inf_step_imp_inf_step_table[OF assms]
  obtain stls where "s -stls→*t ∞" and tls: "tls = lmap (fst ∘ snd) stls" by blast
  from ‹s -stls→*t ∞› have "s -τ-lmap (fst ∘ snd) (lfilter (λ(s, tl, s'). ¬ τmove s tl s') stls)→* ∞"
    by(rule inf_step_table_into_τinf_step)
  hence "s -τ-lnths tls {n. enat n < llength stls ∧ (λ(s, tl, s'). ¬ τmove s tl s') (lnth stls n)}→* ∞"
    unfolding lfilter_conv_lnths tls by simp
  thus ?thesis by blast
qed

lemma silent_moves_into_τrtrancl3p:
  "s -τ→* s' ⟹ s -τ-[]→* s'"
by(induct rule: converse_rtranclp_induct)(blast intro: τrtrancl3p.intros)+

lemma τrtrancl3p_into_silent_moves:
  "s -τ-[]→* s' ⟹ s -τ→* s'"
apply(induct s tls≡"[] :: 'tl list" s' rule: τrtrancl3p.induct)
apply(auto intro: converse_rtranclp_into_rtranclp)
done

lemma τrtrancl3p_Nil_eq_τmoves:
  "s -τ-[]→* s' ⟷ s -τ→* s'"
by(blast intro: silent_moves_into_τrtrancl3p τrtrancl3p_into_silent_moves)

lemma τrtrancl3p_trans [trans]:
  "⟦ s -τ-tls→* s'; s' -τ-tls'→* s'' ⟧ ⟹ s -τ-tls @ tls'→* s''"
apply(induct rule: τrtrancl3p.induct)
apply(auto intro: τrtrancl3p.intros)
done

lemma τrtrancl3p_SingletonE:
  fixes tl
  assumes red: "s -τ-[tl]→* s'''"
  obtains s' s'' where "s -τ→* s'" "s' -tl→ s''" "¬ τmove s' tl s''" "s'' -τ→* s'''"
proof(atomize_elim)
  from red show "∃s' s''. s -τ→* s' ∧ s' -tl→ s'' ∧ ¬ τmove s' tl s'' ∧ s'' -τ→* s'''"
  proof(induct s tls≡"[tl]" s''')
    case (τrtrancl3p_step s s' s'')
    from ‹s -tl→ s'› ‹¬ τmove s tl s'› ‹s' -τ-[]→* s''› show ?case
      by(auto simp add: τrtrancl3p_Nil_eq_τmoves)
   next
    case (τrtrancl3p_τstep s s' s'' tl')
    then obtain t' t'' where "s' -τ→* t'" "t' -tl→ t''" "¬ τmove t' tl t''" "t'' -τ→* s''" by auto
    moreover
    from ‹s -tl'→ s'› ‹τmove s tl' s'› have "s -τ→* s'" by blast
    ultimately show ?case by(auto intro: rtranclp_trans)
  qed
qed

lemma τrtrancl3p_snocI:
  "⋀tl. ⟦ τrtrancl3p s tls s''; s'' -τ→* s'''; s''' -tl→ s'; ¬ τmove s''' tl s' ⟧
  ⟹ τrtrancl3p s (tls @ [tl]) s'"
apply(erule τrtrancl3p_trans)
apply(fold τrtrancl3p_Nil_eq_τmoves)
apply(drule τrtrancl3p_trans)
 apply(erule (1) τrtrancl3p_step)
 apply(rule τrtrancl3p_refl)
apply simp
done

lemma τdiverge_rtranclp_silent_move:
  "⟦ silent_move^** s s'; s' -τ→ ∞ ⟧ ⟹ s -τ→ ∞"
by(induct rule: converse_rtranclp_induct)(auto intro: τdivergeI)

lemma τdiverge_trancl_coinduct [consumes 1, case_names τdiverge]:
  assumes X: "X s"
  and step: "⋀s. X s ⟹ ∃s'. silent_move^++ s s' ∧ (X s' ∨ s' -τ→ ∞)"
  shows "s -τ→ ∞"
proof -
  from X have "∃s'. silent_move^** s s' ∧ X s'" by blast
  thus ?thesis
  proof(coinduct)
    case (τdiverge s)
    then obtain s' where "silent_move⇧*⇧* s s'" "X s'" by blast
    from step[OF ‹X s'›] obtain s'''
      where "silent_move^++ s' s'''" "X s''' ∨ s''' -τ→ ∞" by blast
    from ‹silent_move⇧*⇧* s s'› show ?case
    proof(cases rule: converse_rtranclpE[consumes 1, case_names refl step])
      case refl
      moreover from tranclpD[OF ‹silent_move^++ s' s'''›] obtain s''
        where "silent_move s' s''" "silent_move^** s'' s'''" by blast
      ultimately show ?thesis using ‹silent_move^** s'' s'''› ‹X s''' ∨ s''' -τ→ ∞›
        by(auto intro: τdiverge_rtranclp_silent_move)
    next
      case (step S)
      moreover from ‹silent_move⇧*⇧* S s'› ‹silent_move^++ s' s'''›
      have "silent_move^** S s'''" by(rule rtranclp_trans[OF _ tranclp_into_rtranclp])
      ultimately show ?thesis using ‹X s''' ∨ s''' -τ→ ∞› by(auto intro: τdiverge_rtranclp_silent_move)
    qed
  qed
qed

lemma τdiverge_trancl_measure_coinduct [consumes 2, case_names τdiverge]:
  assumes major: "X s t" "wfP μ"
  and step: "⋀s t. X s t ⟹ ∃s' t'. (μ t' t ∧ s' = s ∨ silent_move^++ s s') ∧ (X s' t' ∨ s' -τ→ ∞)"
  shows "s -τ→ ∞"
proof -
  { fix s t
    assume "X s t"
    with ‹wfP μ› have "∃s' t'. silent_move^++ s s' ∧ (X s' t' ∨ s' -τ→ ∞)"
    proof(induct arbitrary: s rule: wfp_induct[consumes 1])
      case (1 t)
      hence IH: "⋀s' t'. ⟦ μ t' t; X s' t' ⟧ ⟹
                 ∃s'' t''. silent_move^++ s' s'' ∧ (X s'' t'' ∨ s'' -τ→ ∞)" by blast
      from step[OF ‹X s t›] obtain s' t'
        where "μ t' t ∧ s' = s ∨ silent_move⇧+⇧+ s s'" "X s' t' ∨ s' -τ→ ∞" by blast
      from ‹μ t' t ∧ s' = s ∨ silent_move⇧+⇧+ s s'› show ?case
      proof
        assume "μ t' t ∧ s' = s"
        hence  "μ t' t" and [simp]: "s' = s" by simp_all
        from ‹X s' t' ∨ s' -τ→ ∞› show ?thesis
        proof
          assume "X s' t'"
          from IH[OF ‹μ t' t› this] show ?thesis by simp
        next
          assume "s' -τ→ ∞" thus ?thesis
            by cases(auto simp add: silent_move_iff)
        qed
      next
        assume "silent_move⇧+⇧+ s s'"
        thus ?thesis using ‹X s' t' ∨ s' -τ→ ∞› by blast
      qed
    qed }
  note X = this
  from ‹X s t› have "∃t. X s t" ..
  thus ?thesis
  proof(coinduct rule: τdiverge_trancl_coinduct)
    case (τdiverge s)
    then obtain t where "X s t" ..
    from X[OF this] show ?case by blast
  qed
qed

lemma τinf_step2τinf_step_table_LNil [simp]: "τinf_step2τinf_step_table s LNil = LNil"
by(simp add: τinf_step2τinf_step_table_def)

lemma τinf_step2τinf_step_table_LCons [simp]:
  fixes s tl ss tls
  defines "ss ≡ SOME (s', s''). s -τ→* s' ∧ s' -tl→ s'' ∧ ¬ τmove s' tl s'' ∧ s'' -τ-tls→* ∞"
  shows
  "τinf_step2τinf_step_table s (LCons tl tls) =
   LCons (s, fst ss, tl, snd ss) (τinf_step2τinf_step_table (snd ss) tls)"
by(simp add: ss_def τinf_step2τinf_step_table_def split_beta)

lemma lnull_τinf_step2τinf_step_table [simp]:
  "lnull (τinf_step2τinf_step_table s tls) ⟷ lnull tls"
by(simp add: τinf_step2τinf_step_table_def)

lemma lhd_τinf_step2τinf_step_table [simp]:
  "¬ lnull tls ⟹ lhd (τinf_step2τinf_step_table s tls) = 
  (let (s', s'') = SOME (s', s''). s -τ→* s' ∧ s' -lhd tls→ s'' ∧ ¬ τmove s' (lhd tls) s'' ∧ s'' -τ-ltl tls→* ∞
  in (s, s', lhd tls, s''))"
unfolding τinf_step2τinf_step_table_def Let_def by simp

lemma ltl_τinf_step2τinf_step_table [simp]:
  "¬ lnull tls ⟹ ltl (τinf_step2τinf_step_table s tls) =
  (let (s', s'') = SOME (s', s''). s -τ→* s' ∧ s' -lhd tls→ s'' ∧ ¬ τmove s' (lhd tls) s'' ∧ s'' -τ-ltl tls→* ∞
  in τinf_step2τinf_step_table s'' (ltl tls))"
unfolding τinf_step2τinf_step_table_def Let_def
by(simp add: split_beta)

lemma lmap_τinf_step2τinf_step_table: "lmap (fst ∘ snd ∘ snd) (τinf_step2τinf_step_table s tls) = tls"
by(coinduction arbitrary: s tls)(auto simp add: split_beta)

lemma τinf_step_into_τinf_step_table:
  "s -τ-tls→* ∞ ⟹ s -τ-τinf_step2τinf_step_table s tls→*t ∞"
proof(coinduction arbitrary: s tls)
  case (τinf_step_table s tls)
  thus ?case
  proof(cases)
    case (τinf_step_Cons s' s'' tls' tl)
    let ?ss = "SOME (s', s''). s -τ→* s' ∧ s' -tl→ s'' ∧ ¬ τmove s' tl s'' ∧ s'' -τ-tls'→* ∞"
    from τinf_step_Cons have tls: "tls = LCons tl tls'" and "s -τ→* s'" "s' -tl→ s''"
      "¬ τmove s' tl s''" "s'' -τ-tls'→* ∞" by simp_all
    hence "(λ(s', s''). s -τ→* s' ∧ s' -tl→ s'' ∧ ¬ τmove s' tl s'' ∧ s'' -τ-tls'→* ∞) (s', s'')" by simp
    hence "(λ(s', s''). s -τ→* s' ∧ s' -tl→ s'' ∧ ¬ τmove s' tl s'' ∧ s'' -τ-tls'→* ∞) ?ss" by(rule someI)
    with tls have ?τinf_step_table_Cons by auto
    thus ?thesis ..
  next
    case τinf_step_Nil
    then have ?τinf_step_table_Nil by simp
    thus ?thesis ..
  qed
qed

lemma τinf_step_imp_τinf_step_table:
  assumes "s -τ-tls→* ∞"
  shows "∃sstls. s -τ-sstls→*t ∞ ∧ tls = lmap (fst ∘ snd ∘ snd) sstls"
using τinf_step_into_τinf_step_table[OF assms]
by(auto simp only: lmap_τinf_step2τinf_step_table)

lemma τinf_step_table_into_τinf_step:
  "s -τ-sstls→*t ∞ ⟹ s -τ-lmap (fst ∘ snd ∘ snd) sstls→* ∞"
proof(coinduction arbitrary: s sstls)
  case (τinf_step s tls)
  thus ?case by cases(auto simp add: o_def)
qed

lemma silent_move_fromI [intro]:
  "⟦ silent_moves s0 s1; silent_move s1 s2 ⟧ ⟹ silent_move_from s0 s1 s2"
by(simp add: silent_move_from_def)

lemma silent_move_fromE [elim]:
  assumes "silent_move_from s0 s1 s2"
  obtains "silent_moves s0 s1" "silent_move s1 s2"
using assms by(auto simp add: silent_move_from_def)

lemma rtranclp_silent_move_from_imp_silent_moves:
  assumes s'x: "silent_move⇧*⇧* s' x"
  shows "(silent_move_from s')^** x z ⟹ silent_moves s' z"
by(induct rule: rtranclp_induct)(auto intro: s'x)

lemma τdiverge_not_wfP_silent_move_from:
  assumes "s -τ→ ∞"
  shows "¬ wfP (flip (silent_move_from s))"
proof
  assume "wfP (flip (silent_move_from s))"
  moreover define Q where "Q = {s'. silent_moves s s' ∧ s' -τ→ ∞}"
  hence "s ∈ Q" using ‹s -τ→ ∞› by(auto)
  ultimately have "∃z∈Q. ∀y. silent_move_from s z y ⟶ y ∉ Q"
    unfolding wfp_eq_minimal flip_simps by blast
  then obtain z where "z ∈ Q"
    and min: "⋀y. silent_move_from s z y ⟹ y ∉ Q" by blast
  from ‹z ∈ Q› have "silent_moves s z" "z -τ→ ∞" unfolding Q_def by auto
  from ‹z -τ→ ∞› obtain y where "silent_move z y" "y -τ→ ∞" by cases auto
  from ‹silent_moves s z› ‹silent_move z y› have "silent_move_from s z y" ..
  hence "y ∉ Q" by(rule min)
  moreover from ‹silent_moves s z› ‹silent_move z y› ‹y -τ→ ∞›
  have "y ∈ Q" unfolding Q_def by auto
  ultimately show False by contradiction
qed

lemma wfP_silent_move_from_unroll:
  assumes wfPs': "⋀s'. s -τ→ s' ⟹ wfP (flip (silent_move_from s'))"
  shows "wfP (flip (silent_move_from s))"
  unfolding wfp_eq_minimal flip_conv
proof(intro allI impI)
  fix Q and x :: 's
  assume "x ∈ Q"
  show "∃z∈Q. ∀y. silent_move_from s z y ⟶ y ∉ Q"
  proof(cases "∃s'. s -τ→ s' ∧ (∃x'. silent_moves s' x' ∧ x' ∈ Q)")
    case False
    hence "∀y. silent_move_from s x y ⟶ ¬ y ∈ Q"
      by(cases "x=s")(auto, blast elim: converse_rtranclpE intro: rtranclp.rtrancl_into_rtrancl)
    with ‹x ∈ Q› show ?thesis by blast
  next
    case True
    then obtain s' x' where "s -τ→ s'" and "silent_moves s' x'" and "x' ∈ Q"
      by auto
    from ‹s -τ→ s'› have "wfP (flip (silent_move_from s'))" by(rule wfPs')
    from this ‹x' ∈ Q› obtain z where "z ∈ Q" and min: "⋀y. silent_move_from s' z y ⟹ ¬ y ∈ Q"
      and "(silent_move_from s')^** x' z"
      by (rule wfP_minimalE) (unfold flip_simps, blast)
    { fix y
      assume "silent_move_from s z y"
      with ‹(silent_move_from s')^** x' z› ‹silent_move^** s' x'›
      have "silent_move_from s' z y"
        by(blast intro: rtranclp_silent_move_from_imp_silent_moves)
      hence "¬ y ∈ Q" by(rule min) }
    with ‹z ∈ Q› show ?thesis by(auto simp add: intro!: bexI)
  qed
qed

lemma not_wfP_silent_move_from_τdiverge:
  assumes "¬ wfP (flip (silent_move_from s))"
  shows "s -τ→ ∞"
using assms
proof(coinduct)
  case (τdiverge s)
  { assume wfPs': "⋀s'. s -τ→ s' ⟹ wfP (flip (silent_move_from s'))"
    hence "wfP (flip (silent_move_from s))" by(rule wfP_silent_move_from_unroll) }
  with τdiverge have "∃s'. s -τ→ s' ∧ ¬ wfP (flip (silent_move_from s'))" by auto
  thus ?case by blast
qed

lemma τdiverge_neq_wfP_silent_move_from:
  "s -τ→ ∞ ≠ wfP (flip (silent_move_from s))"
by(auto intro: not_wfP_silent_move_from_τdiverge dest: τdiverge_not_wfP_silent_move_from)

lemma not_τdiverge_to_no_τmove:
  assumes "¬ s -τ→ ∞"
  shows "∃s'. s -τ→* s' ∧ (∀s''. ¬ s' -τ→ s'')"
proof -
  define S where "S = s"
  from ‹¬ τdiverge s› have "wfP (flip (silent_move_from S))" unfolding S_def
    using τdiverge_neq_wfP_silent_move_from[of s] by simp
  moreover have "silent_moves S s" unfolding S_def ..
  ultimately show ?thesis
  proof(induct rule: wfp_induct')
    case (wfP s)
    note IH = ‹⋀y. ⟦flip (silent_move_from S) y s; S -τ→* y ⟧
             ⟹ ∃s'. y -τ→* s' ∧ (∀s''. ¬ s' -τ→ s'')›
    show ?case
    proof(cases "∃s'. silent_move s s'")
      case False thus ?thesis by auto
    next
      case True
      then obtain s' where "s -τ→ s'" ..
      with ‹S -τ→* s› have "flip (silent_move_from S) s' s"
        unfolding flip_conv by(rule silent_move_fromI)
      moreover from ‹S -τ→* s› ‹s -τ→ s'› have "S -τ→* s'" ..
      ultimately have "∃s''. s' -τ→* s'' ∧ (∀s'''. ¬ s'' -τ→ s''')" by(rule IH)
      then obtain s'' where "s' -τ→* s''" "∀s'''. ¬ s'' -τ→ s'''" by blast
      from ‹s -τ→ s'› ‹s' -τ→* s''› have "s -τ→* s''" by(rule converse_rtranclp_into_rtranclp)
      with ‹∀s'''. ¬ s'' -τ→ s'''› show ?thesis by blast
    qed
  qed
qed

lemma τdiverge_conv_τRuns:
  "s -τ→ ∞ ⟷ s ⇓ TNil None"
by(auto intro: τRuns.Diverge elim: τRuns.cases)

lemma τinf_step_into_τRuns:
  "s -τ-tls→* ∞ ⟹ s ⇓ tllist_of_llist None tls"
proof(coinduction arbitrary: s tls)
  case (τRuns s tls')
  thus ?case by cases(auto simp add: τdiverge_conv_τRuns)
qed

lemma τ_into_τRuns:
  "⟦ s -τ→ s'; s' ⇓ tls ⟧ ⟹ s ⇓ tls"
by(blast elim: τRuns.cases intro: τRuns.intros τdiverge.intros converse_rtranclp_into_rtranclp)

lemma τrtrancl3p_into_τRuns:
  assumes "s -τ-tls→* s'"
  and "s' ⇓ tls'"
  shows "s ⇓ lappendt (llist_of tls) tls'"
using assms
by induct(auto intro: τRuns.Proceed τ_into_τRuns)

lemma τRuns_table_into_τRuns:
  "τRuns_table s stlsss ⟹ s ⇓ tmap fst id stlsss"
proof(coinduction arbitrary: s stlsss)
  case (τRuns s tls)
  thus ?case by cases(auto simp add: o_def id_def)
qed

definition τRuns2τRuns_table :: "'s ⇒ ('tl, 's option) tllist ⇒ ('tl × 's, 's option) tllist"
where
  "τRuns2τRuns_table s tls = unfold_tllist
     (λ(s, tls). is_TNil tls)
     (λ(s, tls). terminal tls)
     (λ(s, tls). (thd tls, SOME s''. ∃s'. s -τ→* s' ∧ s' -thd tls→ s'' ∧ ¬ τmove s' (thd tls) s'' ∧ s'' ⇓ ttl tls))
     (λ(s, tls). (SOME s''. ∃s'. s -τ→* s' ∧ s' -thd tls→ s'' ∧ ¬ τmove s' (thd tls) s'' ∧ s'' ⇓ ttl tls, ttl tls))
     (s, tls)"

lemma is_TNil_τRuns2τRuns_table [simp]:
  "is_TNil (τRuns2τRuns_table s tls) ⟷ is_TNil tls"
  thm unfold_tllist.disc
by(simp add: τRuns2τRuns_table_def)

lemma thd_τRuns2τRuns_table [simp]:
  "¬ is_TNil tls ⟹
  thd (τRuns2τRuns_table s tls) =
  (thd tls, SOME s''. ∃s'. s -τ→* s' ∧ s' -thd tls→ s'' ∧ ¬ τmove s' (thd tls) s'' ∧ s'' ⇓ ttl tls)"
by(simp add: τRuns2τRuns_table_def)

lemma ttl_τRuns2τRuns_table [simp]:
  "¬ is_TNil tls ⟹
  ttl (τRuns2τRuns_table s tls) =
  τRuns2τRuns_table (SOME s''. ∃s'. s -τ→* s' ∧ s' -thd tls→ s'' ∧ ¬ τmove s' (thd tls) s'' ∧ s'' ⇓ ttl tls) (ttl tls)"
by(simp add: τRuns2τRuns_table_def)

lemma terminal_τRuns2τRuns_table [simp]:
  "is_TNil tls ⟹ terminal (τRuns2τRuns_table s tls) = terminal tls"
by(simp add: τRuns2τRuns_table_def)

lemma τRuns2τRuns_table_simps [simp, nitpick_simp]:
  "τRuns2τRuns_table s (TNil so) = TNil so"
  "⋀tl. 
   τRuns2τRuns_table s (TCons tl tls) =
   (let s'' = SOME s''. ∃s'. s -τ→* s' ∧ s' -tl→ s'' ∧ ¬ τmove s' tl s'' ∧ s'' ⇓ tls
    in TCons (tl, s'') (τRuns2τRuns_table s'' tls))"
 apply(simp add: τRuns2τRuns_table_def)
apply(rule tllist.expand)
apply(simp_all)
done

lemma τRuns2τRuns_table_inverse:
  "tmap fst id (τRuns2τRuns_table s tls) = tls"
by(coinduction arbitrary: s tls) auto
 
lemma τRuns_into_τRuns_table:
  assumes "s ⇓ tls"
  shows "∃stlsss. tls = tmap fst id stlsss ∧ τRuns_table s stlsss"
proof(intro exI conjI)
  from assms show "τRuns_table s (τRuns2τRuns_table s tls)"
  proof(coinduction arbitrary: s tls)
    case (τRuns_table s tls)
    thus ?case
    proof cases
      case (Terminate s')
      hence ?Terminate by simp
      thus ?thesis ..
    next
      case Diverge
      hence ?Diverge by simp
      thus ?thesis by simp
    next
      case (Proceed s' s'' tls' tl)
      let ?P = "λs''. ∃s'. s -τ→* s' ∧ s' -tl→ s'' ∧ ¬ τmove s' tl s'' ∧ s'' ⇓ tls'"
      from Proceed have "?P s''" by auto
      hence "?P (Eps ?P)" by(rule someI)
      hence ?Proceed using ‹tls = TCons tl tls'›
        by(auto simp add: split_beta)
      thus ?thesis by simp
    qed
  qed
qed(simp add: τRuns2τRuns_table_inverse)

lemma τRuns_lappendtE:
  assumes "σ ⇓ lappendt tls tls'"
  and "lfinite tls"
  obtains σ' where "σ -τ-list_of tls→* σ'"
  and "σ' ⇓ tls'"
proof(atomize_elim)
  from ‹lfinite tls› ‹σ ⇓ lappendt tls tls'›
  show "∃σ'. σ -τ-list_of tls→* σ' ∧ σ' ⇓ tls'"
  proof(induct arbitrary: σ)
    case lfinite_LNil thus ?case by(auto intro: τrtrancl3p_refl)
  next
    case (lfinite_LConsI tls tl)
    from ‹σ ⇓ lappendt (LCons tl tls) tls'›
    show ?case unfolding lappendt_LCons
    proof(cases)
      case (Proceed σ' σ'')
      from ‹σ'' ⇓ lappendt tls tls' ⟹ ∃σ'''. σ'' -τ-list_of tls→* σ''' ∧ σ''' ⇓ tls'› ‹σ'' ⇓ lappendt tls tls'›
      obtain σ''' where "σ'' -τ-list_of tls→* σ'''" "σ''' ⇓ tls'" by blast
      from ‹σ' -tl→ σ''› ‹¬ τmove σ' tl σ''› ‹σ'' -τ-list_of tls→* σ'''›
      have "σ' -τ-tl # list_of tls→* σ'''" by(rule τrtrancl3p_step)
      with ‹σ -τ→* σ'› have "σ -τ-[] @ (tl # list_of tls)→* σ'''"
        unfolding τrtrancl3p_Nil_eq_τmoves[symmetric] by(rule τrtrancl3p_trans)
      with ‹lfinite tls› have "σ -τ-list_of (LCons tl tls)→* σ'''" by(simp add: list_of_LCons)
      with ‹σ''' ⇓ tls'› show ?thesis by blast
    qed
  qed
qed

lemma τRuns_total:
  "∃tls. σ ⇓ tls"
proof
  let ?τhalt = "λσ σ'. σ -τ→* σ' ∧ (∀tl σ''. ¬ σ' -tl→ σ'')"
  let ?τdiverge = "λσ. σ -τ→ ∞"
  let ?proceed = "λσ (tl, σ''). ∃σ'. σ -τ→* σ' ∧ σ' -tl→ σ'' ∧ ¬ τmove σ' tl σ''"

  define tls where "tls = unfold_tllist
     (λσ. (∃σ'. ?τhalt σ σ') ∨ ?τdiverge σ)
     (λσ. if ∃σ'. ?τhalt σ σ' then Some (SOME σ'. ?τhalt σ σ') else None)
     (λσ. fst (SOME tlσ'. ?proceed σ tlσ'))
     (λσ. snd (SOME tlσ'. ?proceed σ tlσ')) σ"
  then show "σ ⇓ tls"
  proof(coinduct σ tls rule: τRuns.coinduct)
    case (τRuns σ tls)
    show ?case
    proof(cases "∃σ'. ?τhalt σ σ'")
      case True
      hence "?τhalt σ (SOME σ'. ?τhalt σ σ')" by(rule someI_ex)
      hence ?Terminate using True unfolding τRuns by simp
      thus ?thesis ..
    next
      case False
      note τhalt = this
      show ?thesis
      proof(cases "?τdiverge σ")
        case True
        hence ?Diverge using False unfolding τRuns by simp
        thus ?thesis by simp
      next
        case False
        from not_τdiverge_to_no_τmove[OF this]
        obtain σ' where σ_σ': "σ -τ→* σ'"
          and no_τ: "⋀σ''. ¬ σ' -τ→ σ''" by blast
        from σ_σ' τhalt obtain tl σ'' where "σ' -tl→ σ''" by auto
        moreover with no_τ[of σ''] have "¬ τmove σ' tl σ''" by auto
        ultimately have "?proceed σ (tl, σ'')" using σ_σ' by auto
        hence "?proceed σ (SOME tlσ. ?proceed σ tlσ)" by(rule someI)
        hence ?Proceed using False τhalt unfolding τRuns
          by(subst unfold_tllist.code) fastforce
        thus ?thesis by simp
      qed
    qed
  qed
qed

lemma silent_move2_into_silent_move:
  fixes tl
  assumes "silent_move2 s tl s'"
  shows "s -τ→ s'"
using assms by(auto simp add: silent_move2_def)

lemma silent_move_into_silent_move2:
  assumes "s -τ→ s'"
  shows "∃tl. silent_move2 s tl s'"
using assms by(auto simp add: silent_move2_def)

lemma silent_moves2_into_silent_moves:
  assumes "silent_moves2 s tls s'"
  shows "s -τ→* s'"
using assms
by(induct)(blast intro: silent_move2_into_silent_move rtranclp.rtrancl_into_rtrancl)+

lemma silent_moves_into_silent_moves2:
  assumes "s -τ→* s'"
  shows "∃tls. silent_moves2 s tls s'"
using assms
by(induct)(blast dest: silent_move_into_silent_move2 intro: rtrancl3p_step)+

lemma inf_step_silent_move2_into_τdiverge:
  "trsys.inf_step silent_move2 s tls ⟹ s -τ→ ∞"
proof(coinduction arbitrary: s tls)
  case (τdiverge s)
  thus ?case
    by(cases rule: trsys.inf_step.cases[consumes 1])(auto intro: silent_move2_into_silent_move)
qed

lemma τdiverge_into_inf_step_silent_move2:
  assumes "s -τ→ ∞"
  obtains tls where "trsys.inf_step silent_move2 s tls"
proof -
  define tls where "tls = unfold_llist
     (λ_. False)
     (λs. fst (SOME (tl, s'). silent_move2 s tl s' ∧ s' -τ→ ∞))
     (λs. snd (SOME (tl, s'). silent_move2 s tl s' ∧ s' -τ→ ∞))
     s" (is "_ = ?tls s")
  
  with assms have "s -τ→ ∞ ∧ tls = ?tls s" by simp
  hence "trsys.inf_step silent_move2 s tls"
  proof(coinduct rule: trsys.inf_step.coinduct[consumes 1, case_names inf_step, case_conclusion inf_step step])
    case (inf_step s tls)
    let ?P = "λ(tl, s'). silent_move2 s tl s' ∧ s' -τ→ ∞"
    from inf_step obtain "s -τ→ ∞" and tls: "tls = ?tls s" ..
    from ‹s -τ→ ∞› obtain s' where "s -τ→ s'" "s' -τ→ ∞" by cases
    from ‹s -τ→ s'› obtain tl where "silent_move2 s tl s'" 
      by(blast dest: silent_move_into_silent_move2)
    with ‹s' -τ→ ∞› have "?P (tl, s')" by simp
    hence "?P (Eps ?P)" by(rule someI)
    thus ?case using tls
      by(subst (asm) unfold_llist.code)(auto)
  qed
  thus thesis by(rule that)
qed

lemma τRuns_into_τrtrancl3p:
  assumes runs: "s ⇓ tlss"
  and fin: "tfinite tlss"
  and terminal: "terminal tlss = Some s'"
  shows "τrtrancl3p s (list_of (llist_of_tllist tlss)) s'"
using fin runs terminal
proof(induct arbitrary: s rule: tfinite_induct)
  case TNil thus ?case by cases(auto intro: silent_moves_into_τrtrancl3p)
next
  case (TCons tl tlss)
  from ‹s ⇓ TCons tl tlss› obtain s'' s'''
    where step: "s -τ→* s''"
    and step2: "s'' -tl→ s'''" "¬ τmove s'' tl s'''" 
    and "s''' ⇓ tlss" by cases
  from ‹terminal (TCons tl tlss) = ⌊s'⌋› have "terminal tlss = ⌊s'⌋" by simp
  with ‹s''' ⇓ tlss› have "s''' -τ-list_of (llist_of_tllist tlss)→* s'" by(rule TCons)
  with step2 have "s'' -τ-tl # list_of (llist_of_tllist tlss)→* s'" by(rule τrtrancl3p_step)
  with step have "s -τ-[] @ tl # list_of (llist_of_tllist tlss)→* s'"
    by(rule τrtrancl3p_trans[OF silent_moves_into_τrtrancl3p])
  thus ?case using ‹tfinite tlss› by simp
qed

lemma τRuns_terminal_stuck:
  assumes Runs: "s ⇓ tlss"
  and fin: "tfinite tlss"
  and terminal: "terminal tlss = Some s'"
  and proceed: "s' -tls→ s''"
  shows False
using fin Runs terminal
proof(induct arbitrary: s rule: tfinite_induct)
  case TNil thus ?case using proceed by cases auto
next
  case TCons thus ?case by(fastforce elim: τRuns.cases)
qed

lemma Runs_table_silent_diverge:
  "⟦ Runs_table s stlss; ∀(s, tl, s') ∈ lset stlss. τmove s tl s'; ¬ lfinite stlss ⟧
  ⟹ s -τ→ ∞"
proof(coinduction arbitrary: s stlss)
  case (τdiverge s)
  thus ?case by cases(auto 5 2)
qed

lemma Runs_table_silent_rtrancl:
  assumes "lfinite stlss"
  and "Runs_table s stlss"
  and "∀(s, tl, s') ∈ lset stlss. τmove s tl s'"
  shows "s -τ→* llast (LCons s (lmap (λ(s, tl, s'). s') stlss))" (is ?thesis1)
  and "llast (LCons s (lmap (λ(s, tl, s'). s') stlss)) -tl'→ s'' ⟹ False" (is "PROP ?thesis2")
proof -
  from assms have "?thesis1 ∧ (llast (LCons s (lmap (λ(s, tl, s'). s') stlss)) -tl'→ s'' ⟶ False)"
  proof(induct arbitrary: s)
    case lfinite_LNil thus ?case by(auto elim: Runs_table.cases)
  next
    case (lfinite_LConsI stlss stls)
    from ‹Runs_table s (LCons stls stlss)›
    obtain tl s' where [simp]: "stls = (s, tl, s')"
      and "s -tl→ s'" and Run': "Runs_table s' stlss" by cases
    from ‹∀(s, tl, s')∈lset (LCons stls stlss). τmove s tl s'›
    have "τmove s tl s'" and silent': "∀(s, tl, s')∈lset stlss. τmove s tl s'" by simp_all
    from ‹s -tl→ s'› ‹τmove s tl s'› have "s -τ→ s'" by auto
    moreover from Run' silent'
    have "s' -τ→* llast (LCons s' (lmap (λ(s, tl, s'). s') stlss)) ∧
          (llast (LCons s' (lmap (λ(s, tl, s'). s') stlss)) -tl'→ s'' ⟶ False)"
      by(rule lfinite_LConsI)
    ultimately show ?case by(auto)
  qed
  thus ?thesis1 "PROP ?thesis2" by blast+
qed

lemma Runs_table_silent_lappendD:
  fixes s stlss
  defines "s' ≡ llast (LCons s (lmap (λ(s, tl, s'). s') stlss))"
  assumes Runs: "Runs_table s (lappend stlss stlss')"
  and fin: "lfinite stlss"
  and silent: "∀(s, tl, s') ∈ lset stlss. τmove s tl s'"
  shows "s -τ→* s'" (is ?thesis1)
  and "Runs_table s' stlss'" (is ?thesis2)
  and "stlss' ≠ LNil ⟹ s' = fst (lhd stlss')" (is "PROP ?thesis3")
proof -
  from fin Runs silent
  have "?thesis1 ∧ ?thesis2 ∧ (stlss' ≠ LNil ⟶ s' = fst (lhd stlss'))"
    unfolding s'_def
  proof(induct arbitrary: s)
    case lfinite_LNil thus ?case
      by(auto simp add: neq_LNil_conv Runs_table_simps)
  next
    case lfinite_LConsI thus ?case
      by(clarsimp simp add: neq_LNil_conv Runs_table_simps)(blast intro: converse_rtranclp_into_rtranclp)
  qed
  thus ?thesis1 ?thesis2 "PROP ?thesis3" by simp_all
qed

lemma Runs_table_into_τRuns:
  fixes s stlss
  defines "tls ≡ tmap (λ(s, tl, s'). tl) id (tfilter None (λ(s, tl, s'). ¬ τmove s tl s') (tllist_of_llist (Some (llast (LCons s (lmap (λ(s, tl, s'). s') stlss)))) stlss))"
  (is "_ ≡ ?conv s stlss")
  assumes "Runs_table s stlss"
  shows "τRuns s tls"
using assms
proof(coinduction arbitrary: s tls stlss)
  case (τRuns s tls stlss)
  note tls = ‹tls = ?conv s stlss›
    and Run = ‹Runs_table s stlss›
  show ?case
  proof(cases tls)
    case [simp]: (TNil so)
    from tls
    have silent: "∀(s, tl, s') ∈ lset stlss. τmove s tl s'"
      by(auto simp add: TNil_eq_tmap_conv tfilter_empty_conv)
    show ?thesis
    proof(cases "lfinite stlss")
      case False
      with Run silent have "s -τ→ ∞" by(rule Runs_table_silent_diverge)
      hence ?Diverge using False tls by(simp add: TNil_eq_tmap_conv tfilter_empty_conv)
      thus ?thesis by simp
    next
      case True
      with Runs_table_silent_rtrancl[OF this Run silent]
      have ?Terminate using tls
        by(auto simp add: TNil_eq_tmap_conv tfilter_empty_conv terminal_tllist_of_llist split_def)
      thus ?thesis by simp
    qed
  next
    case [simp]: (TCons tl tls')
    from tls obtain s' s'' stlss' 
      where tl': "tfilter None (λ(s, tl, s'). ¬ τmove s tl s') (tllist_of_llist ⌊llast (LCons s (lmap (λ(s, tl, s'). s') stlss))⌋ stlss) = TCons (s', tl, s'') stlss'"
      and tls': "tls' = tmap (λ(s, tl, s'). tl) id stlss'"
      by(simp add: TCons_eq_tmap_conv split_def id_def split_paired_Ex) blast
    from tfilter_eq_TConsD[OF tl']
    obtain stlsτ rest
      where stlss_eq: "tllist_of_llist ⌊llast (LCons s (lmap (λ(s, tl, s'). s') stlss))⌋ stlss = lappendt stlsτ (TCons (s', tl, s'') rest)"
      and fin: "lfinite stlsτ"
      and silent: "∀(s, tl, s')∈lset stlsτ. τmove s tl s'"
      and "¬ τmove s' tl s''"
      and stlss': "stlss' = tfilter None (λ(s, tl, s'). ¬ τmove s tl s') rest"
      by(auto simp add: split_def)
    from stlss_eq fin obtain rest'
      where stlss: "stlss = lappend stlsτ rest'"
      and rest': "tllist_of_llist ⌊llast (LCons s (lmap (λ(s, tl, s'). s') stlss))⌋ rest' = TCons (s', tl, s'') rest"
      unfolding tllist_of_llist_eq_lappendt_conv by auto
    hence "rest' ≠ LNil" by clarsimp
    from Run[unfolded stlss] fin silent
    have "s -τ→* llast (LCons s (lmap (λ(s, tl, s'). s') stlsτ))"
      and "Runs_table (llast (LCons s (lmap (λ(s, tl, s'). s') stlsτ))) rest'"
      and "llast (LCons s (lmap (λ(s, tl, s'). s') stlsτ)) = fst (lhd rest')"
      by(rule Runs_table_silent_lappendD)+(simp add: ‹rest' ≠ LNil›)
    moreover with rest' ‹rest' ≠ LNil› stlss fin obtain rest''
      where rest': "rest' = LCons (s', tl, s'') rest''"
      and rest: "rest = tllist_of_llist ⌊llast (LCons s'' (lmap (λ(s, tl, s'). s') rest''))⌋ rest''"
      by(clarsimp simp add: neq_LNil_conv llast_LCons lmap_lappend_distrib)
    ultimately have "s -τ→* s'" "s' -tl→ s''" "Runs_table s'' rest''"
      by(simp_all add: Runs_table_simps)
    hence ?Proceed using ‹¬ τmove s' tl s''› tls' stlss' rest
      by(auto simp add: id_def)
    thus ?thesis by simp
  qed
qed

lemma τRuns_table2_into_τRuns:
  "τRuns_table2 s tlsstlss
  ⟹ s ⇓ tmap (λ(tls, s', tl, s''). tl) (λx. case x of Inl (tls, s') ⇒ Some s' | Inr _ ⇒ None) tlsstlss"
proof(coinduction arbitrary: s tlsstlss)
  case (τRuns s tlsstlss)
  thus ?case by cases(auto intro: silent_moves2_into_silent_moves inf_step_silent_move2_into_τdiverge)
qed

lemma τRuns_into_τRuns_table2:
  assumes "s ⇓ tls"
  obtains tlsstlss
  where "τRuns_table2 s tlsstlss"
  and "tls = tmap (λ(tls, s', tl, s''). tl) (λx. case x of Inl (tls, s') ⇒ Some s' | Inr _ ⇒ None) tlsstlss"
proof -
  let ?terminal = "λs tls. case terminal tls of 
          None ⇒ Inr (SOME tls'. trsys.inf_step silent_move2 s tls')
        | Some s' ⇒ let tls' = SOME tls'. silent_moves2 s tls' s' in Inl (tls', s')"
  let ?P = "λs tls (tls'', s', s''). silent_moves2 s tls'' s' ∧ s' -thd tls→ s'' ∧ ¬ τmove s' (thd tls) s'' ∧ s'' ⇓ ttl tls"
  define tlsstlss where "tlsstlss s tls = unfold_tllist
      (λ(s, tls). is_TNil tls)
      (λ(s, tls). ?terminal s tls)
      (λ(s, tls). let (tls'', s', s'') = Eps (?P s tls) in (tls'', s', thd tls, s''))
      (λ(s, tls). let (tls'', s', s'') = Eps (?P s tls) in (s'', ttl tls))
      (s, tls)"
    for s tls

  have [simp]:
    "⋀s tls. is_TNil (tlsstlss s tls) ⟷ is_TNil tls"
    "⋀s tls. is_TNil tls ⟹ terminal (tlsstlss s tls) = ?terminal s tls"
    "⋀s tls. ¬ is_TNil tls ⟹ thd (tlsstlss s tls) = (let (tls'', s', s'') = Eps (?P s tls) in (tls'', s', thd tls, s''))"
    "⋀s tls. ¬ is_TNil tls ⟹ ttl (tlsstlss s tls) = (let (tls'', s', s'') = Eps (?P s tls) in tlsstlss s'' (ttl tls))"
    by(simp_all add: tlsstlss_def split_beta)

  have [simp]:
    "⋀s. tlsstlss s (TNil None) = TNil (Inr (SOME tls'. trsys.inf_step silent_move2 s tls'))"
    "⋀s s'. tlsstlss s (TNil (Some s')) = TNil (Inl (SOME tls'. silent_moves2 s tls' s', s'))"
    unfolding tlsstlss_def by simp_all

  let ?conv = "tmap (λ(tls, s', tl, s''). tl) (λx. case x of Inl (tls, s') ⇒ Some s' | Inr _ ⇒ None)"
  from assms have "τRuns_table2 s (tlsstlss s tls)"
  proof(coinduction arbitrary: s tls)
    case (τRuns_table2 s tls)
    thus ?case
    proof(cases)
      case (Terminate s')
      let ?P = "λtls'. silent_moves2 s tls' s'"
      from ‹s -τ→* s'› obtain tls' where "?P tls'" by(blast dest: silent_moves_into_silent_moves2)
      hence "?P (Eps ?P)" by(rule someI)
      with Terminate have ?Terminate by auto
      thus ?thesis by simp
    next
      case Diverge
      let ?P = "λtls'. trsys.inf_step silent_move2 s tls'"
      from ‹s -τ→ ∞› obtain tls' where "?P tls'" by(rule τdiverge_into_inf_step_silent_move2)
      hence "?P (Eps ?P)" by(rule someI)
      hence ?Diverge using ‹tls = TNil None› by simp
      thus ?thesis by simp
    next
      case (Proceed s' s'' tls' tl)
      from ‹s -τ→* s'› obtain tls'' where "silent_moves2 s tls'' s'"
        by(blast dest: silent_moves_into_silent_moves2)
      with Proceed have "?P s tls (tls'', s', s'')" by simp
      hence "?P s tls (Eps (?P s tls))" by(rule someI)
      hence ?Proceed using Proceed unfolding tlsstlss_def
        by(subst unfold_tllist.code)(auto simp add: split_def)
      thus ?thesis by simp
    qed
  qed
  moreover
  from assms have "tls = ?conv (tlsstlss s tls)"
  proof(coinduction arbitrary: s tls)
    case (Eq_tllist s tls)
    thus ?case
    proof(cases)
      case (Proceed s' s'' tls' tl)
      from ‹s -τ→* s'› obtain tls'' where "silent_moves2 s tls'' s'"
        by(blast dest: silent_moves_into_silent_moves2)
      with Proceed have "?P s tls (tls'', s', s'')" by simp
      hence "?P s tls (Eps (?P s tls))" by(rule someI)
      thus ?thesis using ‹tls = TCons tl tls'› by auto
    qed auto
  qed
  ultimately show thesis by(rule that)
qed

lemma τRuns_table2_into_Runs:
  assumes "τRuns_table2 s tlsstlss"
  shows "Runs s (lconcat (lappend (lmap (λ(tls, s, tl, s'). llist_of (tls @ [tl])) (llist_of_tllist tlsstlss)) (LCons (case terminal tlsstlss of Inl (tls, s') ⇒ llist_of tls | Inr tls ⇒ tls) LNil)))"
  (is "Runs _ (?conv tlsstlss)")
using assms
proof(coinduction arbitrary: s tlsstlss)
  case (Runs s tlsstlss)
  thus ?case
  proof(cases)
    case (Terminate tls' s')
    from ‹silent_moves2 s tls' s'› show ?thesis
    proof(cases rule: rtrancl3p_converseE)
      case refl 
      hence ?Stuck using Terminate by simp
      thus ?thesis ..
    next
      case (step tls'' tl s'')
      from ‹silent_moves2 s'' tls'' s'› ‹⋀tl s''. ¬ s' -tl→ s''›
      have "τRuns_table2 s'' (TNil (Inl (tls'', s')))" ..
      with ‹tls' = tl # tls''› ‹silent_move2 s tl s''› ‹tlsstlss = TNil (Inl (tls', s'))›
      have ?Step by(auto simp add: silent_move2_def intro!: exI)
      thus ?thesis ..
    qed
  next
    case (Diverge tls')
    from ‹trsys.inf_step silent_move2 s tls'›
    obtain tl tls'' s' where "silent_move2 s tl s'" 
      and "tls' = LCons tl tls''" "trsys.inf_step silent_move2 s' tls''"
      by(cases rule: trsys.inf_step.cases[consumes 1]) auto
    from ‹trsys.inf_step silent_move2 s' tls''›
    have "τRuns_table2 s' (TNil (Inr tls''))" ..
    hence ?Step using ‹tlsstlss = TNil (Inr tls')› ‹tls' = LCons tl tls''› ‹silent_move2 s tl s'›
      by(auto simp add: silent_move2_def intro!: exI)
    thus ?thesis ..
  next
    case (Proceed tls' s' s'' tlsstlss' tl)
    from ‹silent_moves2 s tls' s'› have ?Step
    proof(cases rule: rtrancl3p_converseE)
      case refl with Proceed show ?thesis by auto
    next
      case (step tls'' tl' s''')
      from ‹silent_moves2 s''' tls'' s'› ‹s' -tl→ s''› ‹¬ τmove s' tl s''› ‹τRuns_table2 s'' tlsstlss'›
      have "τRuns_table2 s''' (TCons (tls'', s', tl, s'') tlsstlss')" ..
      with ‹tls' = tl' # tls''› ‹silent_move2 s tl' s'''› ‹tlsstlss = TCons (tls', s', tl, s'') tlsstlss'›
      show ?thesis by(auto simp add: silent_move2_def intro!: exI)
    qed
    thus ?thesis ..
  qed
qed

lemma τRuns_table2_silentsD:
  fixes tl
  assumes Runs: "τRuns_table2 s tlsstlss"
  and tset: "(tls, s', tl', s'') ∈ tset tlsstlss"
  and set: "tl ∈ set tls"
  shows "∃s''' s''''. silent_move2 s''' tl s''''"
using tset Runs
proof(induct arbitrary: s rule: tset_induct)
  case (find tlsstlss')
  from ‹τRuns_table2 s (TCons (tls, s', tl', s'') tlsstlss')›
  have "silent_moves2 s tls s'" by cases
  thus ?case using set by induct auto
next
  case step thus ?case by(auto simp add: τRuns_table2_simps)
qed

lemma τRuns_table2_terminal_silentsD:
  assumes Runs: "τRuns_table2 s tlsstlss"
  and fin: "lfinite (llist_of_tllist tlsstlss)"
  and terminal: "terminal tlsstlss = Inl (tls, s'')"
  shows "∃s'. silent_moves2 s' tls s''"
using fin Runs terminal
proof(induct "llist_of_tllist tlsstlss" arbitrary: tlsstlss s)
  case lfinite_LNil thus ?case 
    by(cases tlsstlss)(auto simp add: τRuns_table2_simps)
next
  case (lfinite_LConsI xs tlsstls)
  thus ?case by(cases tlsstlss)(auto simp add: τRuns_table2_simps)
qed

lemma τRuns_table2_terminal_inf_stepD:
  assumes Runs: "τRuns_table2 s tlsstlss"
  and fin: "lfinite (llist_of_tllist tlsstlss)"
  and terminal: "terminal tlsstlss = Inr tls"
  shows "∃s'. trsys.inf_step silent_move2 s' tls"
using fin Runs terminal
proof(induct "llist_of_tllist tlsstlss" arbitrary: s tlsstlss)
  case lfinite_LNil thus ?case
    by(cases tlsstlss)(auto simp add: τRuns_table2_simps)
next
  case (lfinite_LConsI xs tlsstls)
  thus ?case by(cases tlsstlss)(auto simp add: τRuns_table2_simps)
qed

lemma τRuns_table2_lappendtD:
  assumes Runs: "τRuns_table2 s (lappendt tlsstlss tlsstlss')"
  and fin: "lfinite tlsstlss"
  shows "∃s'. τRuns_table2 s' tlsstlss'"
using fin Runs
by(induct arbitrary: s)(auto simp add: τRuns_table2_simps)

end

lemma τmoves_False: "τtrsys.silent_move r (λs ta s'. False) = (λs s'. False)"
by(auto simp add: τtrsys.silent_move_iff)

lemma τrtrancl3p_False_eq_rtrancl3p: "τtrsys.τrtrancl3p r (λs tl s'. False) = rtrancl3p r"
proof(intro ext iffI)
  fix s tls s'
  assume "τtrsys.τrtrancl3p r (λs tl s'. False) s tls s'"
  thus "rtrancl3p r s tls s'" by(rule τtrsys.τrtrancl3p.induct)(blast intro: rtrancl3p_step_converse)+
next
  fix s tls s'
  assume "rtrancl3p r s tls s'"
  thus "τtrsys.τrtrancl3p r (λs tl s'. False) s tls s'"
    by(induct rule: rtrancl3p_converse_induct)(auto intro: τtrsys.τrtrancl3p.intros)
qed

lemma τdiverge_empty_τmove:
  "τtrsys.τdiverge r (λs ta s'. False) = (λs. False)"
by(auto intro!: ext elim: τtrsys.τdiverge.cases τtrsys.silent_move.cases)

end