Theory RR2_Infinite

theory RR2_Infinite
  imports RRn_Automata TR.Tree_Automata_Pumping
begin

lemma ground_ctxt_map_vars_to_adpat:
  assumes "ground_ctxt C"
  shows "map_vars_ctxt f C = adapt_vars_ctxt C" using assms
  by (induct C, auto)
     (metis adapt_vars_def ground_term_to_gtermD map_term_of_gterm)+

lemma [simp]: "map_ta_rule f id r = (r_root r) (map f (r_lhs_states r)) → (f (r_rhs r))" for f r
  by (simp add: ta_rule.expand ta_rule.map_sel(1 - 3))

(* Finitness/Infinitness facts *)
lemma unbound_nat_map:
  assumes "∀ t ∈ S. ∃ u ∈ S. f t < f u" and "S ≠ {}"
  shows "∀(n::nat). ∃t ∈ S. n < f t"
proof -
  obtain x where x: "x ∈ S" using ‹S≠{}› by blast
  from bchoice[of S "λ x y. y ∈ S ∧ f x < f y"] assms obtain g where
    g: "∀ t ∈ S. g t ∈ S ∧ f t < f (g t)" by blast
  define h where "h n = (g^^ (Suc n)) x" for n
  have "n < f (h n) ∧ h n ∈ S" for n
  proof (induct n)
    case 0
    then show ?case using g[THEN bspec, OF x] by (auto simp: h_def)
  next
    case (Suc n) then show ?case using g[THEN bspec, OF conjunct2[OF Suc]]
      by (auto simp: h_def)
  qed
  then show ?thesis by auto
qed

lemma no_upper_bound_infinite:
  assumes "∀(n::nat). ∃t ∈ S. n < f t"
  shows "infinite S"
proof (rule ccontr, simp)
  assume "finite S"
  then obtain n where "n = Max (f ` S)" "∀ t ∈ S. f t ≤ n" by auto
  then show False using assms linorder_not_le by blast
qed

lemma set_constr_finite:
  assumes "finite F"
  shows "finite {h x | x. x ∈ F ∧ P x}" using assms
  by (induct) auto

lemma bounded_depth_finite:
  assumes fin_F: "finite ℱ" and "⋃ (funas_term ` S) ⊆ ℱ"
    and "∀t ∈ S. depth t ≤ n" and "∀t ∈ S. ground t"
  shows "finite S" using assms(2-)
proof (induction n arbitrary: S)
  case 0
  {fix t assume elem: "t ∈ S"
    from 0 have "depth t = 0" "ground t" "funas_term t ⊆ ℱ" using elem by auto
    then have "∃ f. (f, 0) ∈ ℱ ∧ t = Fun f []" by (cases t rule: depth.cases) auto}
  then have "S ⊆ {Fun f [] |f . (f, 0) ∈ ℱ}" by (auto simp add: image_iff)
  from finite_subset[OF this] show ?case
    using set_constr_finite[OF fin_F, of "λ (f, n). Fun f []" "λ x. snd x = 0"]
    by auto
next
  case (Suc n)
  from Suc obtain S' where
    S: "S' = {t :: ('a, 'b) term . ground t ∧ funas_term t ⊆ ℱ ∧ depth t ≤ n}" "finite S'"
    by (auto simp add: SUP_le_iff)
  then obtain L F where L: "set L = S'" "set F = ℱ" using fin_F by (meson finite_list)
  let ?Sn = "{Fun f ts | f ts. (f, length ts) ∈ ℱ ∧ set ts ⊆ S'}"
  let ?Ln = "concat (map (λ (f, n). map (λ ts. Fun f ts) (list_of_permutation_n L n)) F)"
  {fix t assume elem: "t ∈ S"
    from Suc have "depth t ≤ Suc n" "ground t" "funas_term t ⊆ ℱ" using elem by auto
    then have "funas_term t ⊆ ℱ ∧ (∀ x ∈ set (args t). depth x ≤ n) ∧ ground t"
      by (cases t rule: depth.cases) auto
    then have "t ∈ ?Sn ∪ S'"
      using S by (cases t) auto} note sub = this
  {fix t assume elem: "t ∈ ?Sn"
    then obtain f ts where [simp]: "t = Fun f ts" and invar: "(f, length ts) ∈ ℱ" "set ts ⊆ S'"
      by blast
    then have "Fun f ts ∈ set (map (λ ts. Fun f ts) (list_of_permutation_n L (length ts)))"
      using list_fun_sym_eq_set[of L "length ts"] L by (auto simp: image_iff) 
    then have "t ∈ set ?Ln" using invar(1) L(2) by auto}
  from this sub have sub: "?Sn ⊆ set ?Ln" "S ⊆ ?Sn ∪ S'" by blast+
  from finite_subset[OF sub(1)] finite_subset[OF sub(2)] finite_UnI[of ?Sn, OF _ S(2)]
  show ?case by blast
qed

lemma infinite_set_dec_infinite:
  assumes "infinite S" and "⋀ s. s ∈ S ⟹ ∃ t. f t = s ∧ P t"
  shows "infinite {t | t s. s ∈ S ∧ f t = s ∧ P t}" (is "infinite ?T")
proof (rule ccontr)
  assume ass: "¬ infinite ?T"
  have "S ⊆ f ` {x . P x}" using assms(2) by auto 
  then show False using ass assms(1)
    by (auto simp: subset_image_iff)
      (smt Ball_Collect finite_imageI image_subset_iff infinite_iff_countable_subset subset_eq) 
qed

lemma infinite_inj_image_infinite:
  assumes "infinite S" and "inj_on f S"
  shows "infinite (f ` S)"
  using assms finite_image_iff by blast

lemma infinite_set_restrict_to_property:
  assumes "⋀ x. x ∈ S ⟹ P x" "infinite S"
  shows "infinite {t| t. P t}" using assms
  by (metis (mono_tags, lifting) Ball_Collect in_mono infinite_iff_countable_subset)

lemma infinite_presev_remove_prop:
  assumes "infinite {t. P t ∧ Q t}"
  shows "infinite {t. P t}"
  using assms by auto

(*The following lemma tells us that number of terms greater than a certain depth are infinite*)
lemma infinte_no_depth_limit:
  assumes "infinite S" and "finite ℱ"
    and "∀t ∈ S. funas_term t ⊆ ℱ" and "∀t ∈ S. ground t"
  shows "∀(n::nat). ∃t ∈ S. n < (depth t)"
proof(rule allI, rule ccontr)
  fix n::nat
  assume "¬ (∃t ∈ S. (depth t) >  n)"
  hence "∀t ∈ S. depth t ≤ n" by auto
  from bounded_depth_finite[OF assms(2) _ this] show False using assms
    by auto
qed

lemma inf_ground_terms_to_gterms:
  assumes "infinite {t . ground t ∧ P t}" (is "infinite ?T")
  shows "infinite {t .  P (term_of_gterm t)}" (is "infinite ?S")
proof -
  have "inj_on gterm_of_term {t. ground t ∧ P t}" using gterm_of_term_inv by (fastforce simp: inj_on_def)
  from infinite_inj_image_infinite[OF assms this] show ?thesis unfolding image_Collect
    by auto (smt Collect_cong ground_term_of_gterm gterm_of_term_inv term_of_gterm_inv)
qed


lemma depth_gterm_conv:
  shows "depth (term_of_gterm t) = depth (term_of_gterm t)"
  by (metis leD nat_neq_iff poss_gposs_conv poss_length_bounded_by_depth poss_length_depth)

lemma funs_term_ctxt [simp]:
  "funs_term C⟨s⟩ = funs_ctxt C ∪ funs_term s"
  by (induct C) auto


"rule_st t 𝒜 q = (∃ qs. (fst (the (root t))) qs → q |∈| rules 𝒜 ∧">definition "rule_st t 𝒜 q = (∃ qs. (fst (the (root t))) qs → q |∈| rules 𝒜 ∧
  length qs = length (args t) ∧
  (∀ i < length (args t). qs ! i |∈| ta_der 𝒜 (args t ! i)))"

lemma ta_der_to_rule_st:
  assumes "q |∈| ta_der 𝒜 t" and "is_Fun t"
  obtains p where "rule_st t 𝒜 p" "p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+|"
  using assms by (cases t) (auto simp: rule_st_def)

lemma ta_der_to_rule_st_ground:
  assumes "q |∈| ta_der 𝒜 t" and "ground t"
  obtains p where "rule_st t 𝒜 p" "p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+|"
  using assms by (cases t) (auto simp: rule_st_def)

lemma rule_st_res:
  assumes "rule_st t 𝒜 p" and "is_Fun t"
  shows "p |∈| ta_der 𝒜 t"
  using assms by (cases t) (auto simp: rule_st_def)

lemma rule_st_res_ground:
  assumes "rule_st t 𝒜 p" and "ground t"
  shows "p |∈| ta_der 𝒜 t"
  using assms by (cases t) (auto simp: rule_st_def)

lemma rule_st_ctxt:
  assumes "rule_st C⟨Var q⟩ 𝒜 p" "q |∈| ta_der 𝒜 t" and "C ≠ □"
  shows "rule_st C⟨t⟩ 𝒜 p" using assms
proof (induct C)
  case (More f ss C ts)
  then show ?case by (auto simp: rule_st_def) (metis append_Cons_nth_not_middle nth_append_length ta_der_ctxt)
qed auto

lemma pigeonhole_ta_infinit_terms:
  assumes "fcard (𝒬 𝒜) < depth t" and "q |∈| ta_der 𝒜 t"
    and "ground t" and "P (funas_term t)"
  shows "infinite {t . q |∈| ta_der 𝒜 t ∧ ground t ∧ P (funas_term t)}"
proof -
  from pigeonhole_tree_automata[OF assms(1 - 3)]
  obtain C C2 s v p where ctxt: "C2 ≠ □" "C⟨s⟩ = t" "C2⟨v⟩ = s" and
    loop: "p |∈| ta_der 𝒜 v" "p |∈| ta_der 𝒜 C2⟨Var p⟩" "q |∈| ta_der 𝒜 C⟨Var p⟩" by blast
  let ?terms = "λ n. C⟨(C2 ^n)⟨v⟩⟩" let ?inner = "λ n. (C2 ^n)⟨v⟩"
  have gr: "ground_ctxt C2" "ground_ctxt C" "ground v" using ctxt assms(3)
    by (metis ground_ctxt_apply)+
  have "q |∈| ta_der 𝒜  (C ∘⇩c C2)⟨Var p⟩" "is_Fun (C ∘⇩c C2)⟨Var p⟩" using ctxt loop assms(2)
    by (auto simp: ta_der_ctxt) (metis Var_supt ctxt.cop_add ctxt_comp_rhs_not_hole is_Var_def nectxt_imp_supt_ctxt) 
  let ?P = "λ t. q |∈| ta_der 𝒜 t ∧ ground t ∧ P (funas_term t)"
  from ctxt have "t ⊳ v" using ctxt_comp_rhs_not_hole ctxt_ctxt
    by (metis ctxt.cop_add ctxt_supt)
  moreover have "P (funas_term (?terms (Suc n)))" for n using ctxt assms(4)
    by (auto simp: vars_term_ctxt_apply) (metis Un_absorb2 ctxt_comp_n_pres_funas sup.idem sup.orderI sup_assoc)
  moreover have "q |∈| ta_der 𝒜 (?terms (Suc n))" for n using loop
    by auto (meson ta_der_ctxt ta_der_ctxt_n_loop) 
  ultimately have "?P (?terms (Suc n))" for n using gr
    by (metis ctxt_comp_n_pres_ground ground_ctxt_apply)
  then show ?thesis
    using order.strict_trans2[OF ctxt_comp_n_lower_bound[OF ctxt(1)] depth_ctxt_less_eq[of "?inner (Suc n)" C for n]]
    using no_upper_bound_infinite[of _ depth, of "{t. q |∈| ta_der 𝒜 t ∧ ground t ∧ P (funas_term t)}"]
     by blast
qed


lemma gterm_to_None_Some_funas [simp]:
  "funas_gterm (gterm_to_None_Some t) ⊆ (λ (f, n). ((None, Some f), n)) ` ℱ ⟷ funas_gterm t ⊆ ℱ"
  by (induct t) (auto simp: funas_gterm_def, blast)

lemma funas_gterm_bot_some_decomp:
  assumes "funas_gterm s ⊆ (λ (f, n). ((None, Some f), n)) ` ℱ"
  shows "∃ t. gterm_to_None_Some t = s" using assms
proof (induct s)
  case (GFun f ts)
  from GFun(1)[OF nth_mem] obtain ss where "length ss = length ts ∧ (∀i<length ts. gterm_to_None_Some (ss ! i) = ts ! i)"
    using Ex_list_of_length_P[of "length ts" "λ s i. gterm_to_None_Some s = ts ! i"] GFun(2-)
    by (auto simp: funas_gterm_def) (meson UN_subset_iff nth_mem) 
  then show ?case using GFun(2-)
    by (cases f) (auto simp: funas_gterm_def map_nth_eq_conv intro: exI[of _ "GFun (the (snd f)) ss"])
qed

(* Definition INF, Q_infinity and automata construction *)

"Inf_branching_terms ℛ ℱ = {t . infinite {u. (t, u) ∈ ℛ ∧ funas_gterm u ⊆ fset ℱ} ∧ funas_gterm t ⊆ fset ℱ}"">definition "Inf_branching_terms ℛ ℱ = {t . infinite {u. (t, u) ∈ ℛ ∧ funas_gterm u ⊆ fset ℱ} ∧ funas_gterm t ⊆ fset ℱ}"

"Q_infty 𝒜 ℱ = {|q | q. infinite {t | t. funas_gterm t ⊆ fset ℱ ∧ q |∈| ta_der 𝒜 (term_of_gterm (gterm_to_None_Some t))}|}"">definition "Q_infty 𝒜 ℱ = {|q | q. infinite {t | t. funas_gterm t ⊆ fset ℱ ∧ q |∈| ta_der 𝒜 (term_of_gterm (gterm_to_None_Some t))}|}"

lemma Q_infty_fmember:
  "q |∈| Q_infty 𝒜 ℱ ⟷ infinite {t | t. funas_gterm t ⊆ fset ℱ ∧ q |∈| ta_der 𝒜 (term_of_gterm (gterm_to_None_Some t))}"
proof -
  have "{q | q. infinite {t | t. funas_gterm t ⊆ fset ℱ ∧ q |∈| ta_der 𝒜 (term_of_gterm (gterm_to_None_Some t))}} ⊆ fset (𝒬 𝒜)"
    using not_finite_existsD notin_fset by fastforce
  from finite_subset[OF this] show ?thesis
    by (auto simp: Q_infty_def)
qed

abbreviation q_inf_dash_intro_rules where
  "q_inf_dash_intro_rules Q r ≡ if (r_rhs r) |∈| Q ∧ fst (r_root r) = None then {|(r_root r) (map CInl (r_lhs_states r)) → CInr (r_rhs r)|} else {||}"

abbreviation args :: "'a list ⇒ nat ⇒ ('a + 'a) list" where
  "args ≡ λ qs i. map CInl (take i qs) @ CInr (qs ! i) # map CInl (drop (Suc i) qs)"

abbreviation q_inf_dash_closure_rules :: "('q, 'f) ta_rule ⇒ ('q + 'q, 'f) ta_rule list" where
  "q_inf_dash_closure_rules r ≡ (let (f, qs, q) = (r_root r, r_lhs_states r, r_rhs r) in
   (map (λ i. f (args qs i) → CInr q) [0 ..< length qs]))"

definition Inf_automata :: "('q, 'f option × 'f option) ta ⇒ 'q fset ⇒ ('q + 'q, 'f option × 'f option) ta" where
  "Inf_automata 𝒜 Q = TA
  (( |⋃| (q_inf_dash_intro_rules Q |`| rules 𝒜)) |∪| ( |⋃| ((fset_of_list ∘ q_inf_dash_closure_rules) |`| rules 𝒜)) |∪|
   map_ta_rule CInl id |`| rules 𝒜) (map_both Inl |`| eps 𝒜 |∪| map_both CInr |`| eps 𝒜)"

definition Inf_reg where
  "Inf_reg 𝒜 Q = Reg (CInr |`| fin 𝒜) (Inf_automata (ta 𝒜) Q)"

lemma Inr_Inl_rel_comp:
  "map_both CInr |`| S |O| map_both CInl |`| S = {||}" by auto

lemmas eps_split = ftrancl_Un2_separatorE[OF Inr_Inl_rel_comp]

lemma Inf_automata_eps_simp [simp]:
  shows "(map_both Inl |`| eps 𝒜 |∪| map_both CInr |`| eps 𝒜)|⇧+| =
      (map_both CInl |`| eps 𝒜)|⇧+| |∪| (map_both CInr |`| eps 𝒜)|⇧+|"
proof -
  {fix x y z assume "(x, y) |∈| (map_both CInl |`| eps 𝒜)|⇧+|"
    "(y, z) |∈| (map_both CInr |`| eps 𝒜)|⇧+|"
    then have False
      by (metis Inl_Inr_False eps_statesI(1, 2) eps_states_image fimageE ftranclD ftranclD2)}
  then show ?thesis by (auto simp: Inf_automata_def eps_split)
qed

lemma map_both_CInl_ftrancl_conv:
  "(map_both CInl |`| eps 𝒜)|⇧+| = map_both CInl |`| (eps 𝒜)|⇧+|"
  "(map_both CInr |`| eps 𝒜)|⇧+| = map_both CInr |`| (eps 𝒜)|⇧+|"
  by (auto simp: finj_CInl_CInr ftrancl_map_both fmap_prod_fimageI)

lemma Inf_automata_Inl_to_eps [simp]:
  "(CInl p, CInl q) |∈| (map_both CInl |`| eps 𝒜)|⇧+| ⟷ (p, q) |∈| (eps 𝒜)|⇧+|"
  "(CInr p, CInr q) |∈| (map_both CInr |`| eps 𝒜)|⇧+| ⟷ (p, q) |∈| (eps 𝒜)|⇧+|"
  "(CInl q, CInl p) |∈| (map_both CInr |`| eps 𝒜)|⇧+| ⟷ False"
  "(CInr q, CInr p) |∈| (map_both CInl |`| eps 𝒜)|⇧+| ⟷ False"
  by (auto simp: finj_CInl_CInr ftrancl_map_both fmap_prod_fimageI)

lemma Inl_eps_Inr:
  "(CInl q, CInl p) |∈| (eps (Inf_automata 𝒜 Q))|⇧+| ⟷ (CInr q, CInr p) |∈| (eps (Inf_automata 𝒜 Q))|⇧+|"
  by (auto simp: Inf_automata_def)

lemma Inr_rhs_eps_Inr_lhs:
  assumes "(q, CInr p) |∈| (eps (Inf_automata 𝒜 Q))|⇧+|"
  obtains q' where "q = CInr q'" using assms
  by (cases q) (auto simp: Inf_automata_def finj_CInl_CInr ftrancl_map_both)

lemma Inl_rhs_eps_Inl_lhs:
  assumes "(q, CInl p) |∈| (eps (Inf_automata 𝒜 Q))|⇧+|"
  obtains q' where "q = CInl q'" using assms
  by (cases q) (auto simp: Inf_automata_def finj_CInl_CInr ftrancl_map_both)

lemma Inf_automata_eps [simp]:
  "(CInl q, CInr p) |∈| (eps (Inf_automata 𝒜 Q))|⇧+| ⟷ False"
  "(CInr q, CInl p) |∈| (eps (Inf_automata 𝒜 Q))|⇧+| ⟷ False"
  by (auto elim: Inr_rhs_eps_Inr_lhs Inl_rhs_eps_Inl_lhs)

lemma Inl_A_res_Inf_automata:
  "ta_der (fmap_states_ta CInl 𝒜) t |⊆| ta_der (Inf_automata 𝒜 Q) t"
  by (intro ta_der_mono) (auto simp: Inf_automata_def rev_fimage_eqI fmap_states_ta_def')

lemma Inl_res_A_res_Inf_automata:
  "CInl |`| ta_der 𝒜 (term_of_gterm t) |⊆| ta_der (Inf_automata 𝒜 Q) (term_of_gterm t)"
  by (intro fsubset_trans[OF ta_der_fmap_states_ta_mono[of CInl 𝒜 t]]) (auto simp: Inl_A_res_Inf_automata)

lemma r_rhs_CInl_args_A_rule:
  assumes "f qs → CInl q |∈| rules (Inf_automata 𝒜 Q)"
  obtains qs' where "qs = map CInl qs'" "f qs' → q |∈| rules 𝒜" using assms
  by (auto simp: Inf_automata_def split!: if_splits)

lemma A_rule_to_dash_closure:
  assumes "f qs → q |∈| rules 𝒜" and "i < length qs"
  shows "f (args qs i) → CInr q |∈| rules (Inf_automata 𝒜 Q)"
  using assms by (auto simp add: Inf_automata_def fimage_iff fBall_def upt_fset intro!: fBexI[OF _ assms(1)])

lemma Inf_automata_reach_to_dash_reach:
  assumes "CInl p |∈| ta_der (Inf_automata 𝒜 Q) C⟨Var (CInl q)⟩"
  shows "CInr p |∈| ta_der (Inf_automata 𝒜 Q) C⟨Var (CInr q)⟩" (is "_ |∈| ta_der ?A _")
  using assms
proof (induct C arbitrary: p)
  case (More f ss C ts)
  from More(2) obtain qs q' where
    rule: "f qs → q' |∈| rules ?A" "length qs = Suc (length ss + length ts)" and
    eps: "q' = CInl p ∨ (q', CInl p) |∈| (eps ?A)|⇧+|" and
    reach: "∀ i <  Suc (length ss + length ts). qs ! i |∈| ta_der ?A ((ss @ C⟨Var (CInl q)⟩ # ts) ! i)"
    by (auto simp: map_append_Cons_nth)
  from eps obtain q'' where [simp]: "q' = CInl q''"
    by (cases q') (auto simp add: Inf_automata_def eps_split elim: ftranclE converse_ftranclE)
  from rule obtain qs' where args: "qs = map CInl qs'" "f qs' → q'' |∈| rules 𝒜"
    using r_rhs_CInl_args_A_rule by (metis ‹q' = CInl q''›)
  then have "CInl (qs' ! length ss) |∈| ta_der (Inf_automata 𝒜 Q) C⟨Var (CInl q)⟩" using reach
    by (auto simp: all_Suc_conv nth_append_Cons) (metis length_map less_add_Suc1 local.rule(2) nth_append_length nth_map reach) 
  from More(1)[OF this] More(2) show ?case
    using rule args eps reach A_rule_to_dash_closure[OF args(2), of "length ss" Q]
    by (auto simp: map_append_Cons_nth Inl_eps_Inr id_take_nth_drop all_Suc_conv
        intro!: exI[of _ "CInr q''"] exI[of _ "map CInl (take (length ss) qs') @ CInr (qs' ! length ss) # map CInl (drop (Suc (length ss)) qs')"])
      (auto simp: nth_append_Cons min_def)
qed (auto simp: Inf_automata_def)

lemma res_rule_st_Inf_automata_dash:
  assumes "rule_st (term_of_gterm (gterm_to_None_Some t)) 𝒜 p" and "p |∈| Q"
  shows "CInr p |∈| ta_der (Inf_automata 𝒜 Q) (term_of_gterm (gterm_to_None_Some t))" (is "CInr p |∈| ta_der ?A _")
proof (cases t)
  case [simp]: (GFun f ts)
  from rule_st_res[OF assms(1)] assms(1) obtain qs where
    rule: "(None, Some f) qs → p |∈| rules 𝒜" "length qs = length ts" and
    reach: "∀ i < length ts. qs ! i |∈| ta_der 𝒜 (term_of_gterm (gterm_to_None_Some (ts  ! i)))"
    by (auto simp: map_append_Cons_nth rule_st_def)
  from rule assms(2) have "(None, Some f) (map CInl qs) → CInr p |∈| rules ?A"
    by (auto simp: Inf_automata_def) force
  then show ?thesis using reach rule Inl_res_A_res_Inf_automata[of 𝒜 "gterm_to_None_Some (ts ! i)" Q for i]
    by (auto intro!: exI[of _ "CInr p"]  exI[of _ "map CInl qs"]) blast
qed

lemma Inf_automata_dash_reach_to_reach:
  assumes "p |∈| ta_der (Inf_automata 𝒜 Q) t" (is "_ |∈| ta_der ?A _")
  shows "remove_sum p |∈| ta_der 𝒜 (map_vars_term remove_sum t)" using assms
proof (induct t arbitrary: p)
  case (Var x) then show ?case
    by (cases p; cases x) (auto simp: map_both_CInl_ftrancl_conv Inf_automata_def inj_CInl ftrancl_map_both)
next
  case (Fun f ss)
  from Fun(2) obtain qs q' where
    rule: "f qs → q' |∈| rules ?A" "length qs = length ss" and
    eps: "q' = p ∨ (q', p) |∈| (eps ?A)|⇧+|" and
    reach: "∀ i <  length ss. qs ! i |∈| ta_der ?A (ss ! i)" by auto
  from rule have r: "f (map (remove_sum) qs) → (remove_sum q') |∈| rules 𝒜"
    by (auto simp: comp_def Inf_automata_def min_def id_take_nth_drop[symmetric] upt_fset
             simp flip: drop_map take_map split!: if_splits)
  moreover have "remove_sum q' = remove_sum p ∨ (remove_sum q', remove_sum p) |∈| (eps 𝒜)|⇧+|" using eps
    by (cases "is_Inl q'"; cases "is_Inl p") (auto elim!: is_InlE is_InrE, auto simp: Inf_automata_def)
  ultimately show ?case using reach rule(2) Fun(1)[OF nth_mem, of i "qs ! i" for i]
    by auto (metis (mono_tags, lifting) length_map map_nth_eq_conv)+
qed

lemma depth_poss_split:
  assumes "Suc (depth (term_of_gterm t) + n) < depth (term_of_gterm u)"
  shows "∃ p q. p @ q ∈ gposs u ∧ n < length q ∧ p ∉ gposs t"
proof -
  from poss_length_depth obtain p m where p: "p ∈ gposs u" "length p = m" "depth (term_of_gterm u) = m"  using poss_gposs_conv by blast
  then obtain m' where dt: "depth (term_of_gterm t) = m'" by blast
  have nt: "take (Suc m') p ∉ gposs t" using poss_length_bounded_by_depth dt depth_gterm_conv
    by (metis Suc_leI add_Suc_right add_lessD1 assms leD length_take lessI min.absorb2 p(2, 3))
  moreover have "n < length (drop (Suc m') p)" using assms depth_gterm_conv dt p(2-)
    by (metis add_Suc diff_diff_left length_drop zero_less_diff) 
  ultimately show ?thesis by (metis append_take_drop_id p(1))
qed

lemma gpair_poss_lang_split_ctxt_rule_st:
  assumes "p ∈ gposs (gpair t u)" and "gpair t u ∈ gta_lang Q 𝒜"
  shows "∃ q q'. CInl q |∈| CInl |`| Q ∧
    CInl q |∈| ta_der (fmap_states_ta CInl 𝒜) (term_of_gterm (gpair t u)) ∧
    rule_st (term_of_gterm (gsubt_at (gpair t u) p)) 𝒜 q' ∧
    CInl q' |∈| ta_der (fmap_states_ta CInl 𝒜) (term_of_gterm (gsubt_at (gpair t u) p)) ∧
    CInl q |∈| ta_der (fmap_states_ta CInl 𝒜) (ctxt_of_pos_term p (term_of_gterm (gpair t u)))⟨Var (CInl q')⟩"
proof -
  let ?t_of_g = "λ t. term_of_gterm t :: ('a option × 'b option, 'c + 'c) term"
  define C where "(C :: ('a option × 'b option, 'c + 'c) ctxt) = ctxt_of_pos_term p (?t_of_g (gpair t u))"
  then have gp_ctxt: "gterm_of_term C⟨term_of_gterm (gsubt_at (gpair t u) p)⟩ = gpair t u"
    using assms(1) ctxt_of_pos_gterm_gsubt_at_to_gterm gpair_poss_args_poss poss_append_poss by blast
  then have gr_ctxt: "ground_ctxt C" using assms(1) unfolding C_def
    by (metis ctxt_supt_id ground_ctxt_apply ground_term_of_gterm poss_gposs_conv)
  then have gr_term: "ground C⟨term_of_gterm (gsubt_at (gpair t u) p)⟩"
    using ground_ctxt_apply ground_term_of_gterm by blast
  obtain q' where lang: "CInl q' |∈| CInl |`| Q"  
    "CInl q' |∈| ta_der (fmap_states_ta CInl 𝒜) (term_of_gterm (gpair t u))"
    using assms(2) ta_der_fmap_states_ta_mono[of CInl 𝒜 "gpair t u"]
    by (auto elim!: gta_langE)
  from lang(2) have reach_fin: "CInl q' |∈| ta_der (fmap_states_ta CInl 𝒜) C⟨term_of_gterm (gsubt_at (gpair t u) p)⟩"
    using gp_ctxt gr_term gterm_of_term_inv by fastforce
  obtain q where reach_CInl: "CInl q |∈| ta_der (fmap_states_ta CInl 𝒜) (term_of_gterm (gsubt_at (gpair t u) p))"
    "CInl q' |∈| ta_der (fmap_states_ta CInl 𝒜) C⟨Var (CInl q)⟩"
    using ta_der_ctxt_decompose[OF reach_fin]
    by auto (metis (no_types, lifting) fimageE fmap_states gterm_ta_der_states)

  then have "q |∈| ta_der 𝒜 (term_of_gterm (gsubt_at (gpair t u) p))"
    using ta_der_fmap_states_ta_mono2[of CInl] inj_CInl by (simp add: finj_CInl_CInr) blast
  from ta_der_to_rule_st_ground[OF this] obtain q'' where
    rule_st: "rule_st (term_of_gterm (gsubt_at (gpair t u) p)) 𝒜 q''" and
    eps: "q'' = q ∨ (q'', q) |∈| (eps 𝒜)|⇧+|" by auto
  from rule_st_res_ground[OF rule_st] have reach: "q'' |∈| ta_der 𝒜 (term_of_gterm (gsubt_at (gpair t u) p))" by auto
  then have r: "CInl q'' |∈| ta_der (fmap_states_ta CInl 𝒜) (term_of_gterm (gsubt_at (gpair t u) p))"
    "q'' = q ∨ (CInl q'', CInl q) |∈| (eps (fmap_states_ta CInl 𝒜))|⇧+|"
    using ta_der_fmap_states_ta_mono[of CInl 𝒜 "gsubt_at (gpair t u) p"]
    by blast (auto simp: fmap_states_ta_def' eps) 
  then show ?thesis using lang reach_CInl C_def rule_st ta_der_eps_ctxt[of _ _ _ "CInl q"] r(2)
    by blast
qed

lemma Inf_to_automata:
  assumes "RR2_spec 𝒜 ℛ" and "t ∈ Inf_branching_terms ℛ ℱ"
  shows "∃ u. gpair t u ∈ ℒ (Inf_reg 𝒜 (Q_infty (ta 𝒜) ℱ))" (is "∃ u. gpair t u ∈ ℒ ?B")
proof -
  let ?A = "Inf_automata (ta 𝒜) (Q_infty (ta 𝒜) ℱ)"
  let ?t_of_g = "λ t. term_of_gterm t :: ('b, 'a) term"
  let ?t_of_gp = "λ t. term_of_gterm t :: ('b option × 'b option, 'a) term"
  let ?none_t = "λ t. term_of_gterm (gterm_to_None_Some t) :: ('b option × 'b option, 'a) term"
  obtain n where depth_card: "depth (?t_of_g t) + fcard (𝒬 (ta 𝒜)) < n" by auto
  from assms(1, 2) have fin: "infinite {u. gpair t u ∈ ℒ 𝒜 ∧ funas_gterm u ⊆ fset ℱ}"
    by (auto simp: RR2_spec_def Inf_branching_terms_def)
  from infinte_no_depth_limit[of "?t_of_g ` {u. gpair t u ∈ ℒ 𝒜 ∧ funas_gterm u ⊆ fset ℱ}" "fset ℱ"] this
  have "∀ n. ∃t ∈ ?t_of_g ` {u. gpair t u ∈ ℒ 𝒜 ∧ funas_gterm u ⊆ fset ℱ}. n < depth t"
    by (simp add: infinite_inj_image_infinite[OF fin] funas_term_of_gterm_conv inj_term_of_gterm)
  from this depth_card obtain u where funas: "funas_gterm u ⊆ fset ℱ" and
    depth: "Suc n < depth (?t_of_g u)" and lang: "gpair t u ∈ ℒ 𝒜" by auto
  have "Suc (depth (term_of_gterm t) + fcard (𝒬 (ta 𝒜))) < depth (term_of_gterm u)"
    using depth depth_card by (metis Suc_less_eq2 depth_gterm_conv less_trans)
  from depth_poss_split[OF this] obtain p q where
    pos: "p @ q ∈ gposs u ∧ fcard (𝒬 (ta 𝒜)) < length q ∧ p ∉ gposs t" by auto
  then have gp: "gsubt_at (gpair t u) p = gterm_to_None_Some (gsubt_at u p)" by auto
  define C where "(C :: ('b option × 'b option, 'a + 'a) ctxt) = ctxt_of_pos_term p (term_of_gterm (gpair t u))"
  have gp_split: "gterm_of_term C⟨term_of_gterm (gsubt_at (gpair t u) p)⟩ = gpair t u" unfolding C_def
    using ctxt_of_pos_gterm_gsubt_at_to_gterm gpair_poss_args_poss poss_append_poss pos by blast
  have gr_ctxt: "ground_ctxt C" using pos unfolding C_def
    by (metis ctxt_supt_id gpair_poss_args_poss ground_ctxt_apply ground_term_of_gterm poss_append_poss poss_gposs_conv)
  from pos gpair_poss_lang_split_ctxt_rule_st[OF _ lang[unfolded ℒ_def]] obtain q' q'' where
    lang: "CInl q' |∈| CInl |`| fin 𝒜" "CInl q' |∈| ta_der (fmap_states_ta CInl (ta 𝒜)) (term_of_gterm (gpair t u))" and
    rule_st: "rule_st (term_of_gterm (gsubt_at (gpair t u) p)) (ta 𝒜) q''" and
    reach_rule_st: "CInl q'' |∈| ta_der (fmap_states_ta CInl (ta 𝒜)) (term_of_gterm (gsubt_at (gpair t u) p))" and
    reach_fin: "CInl q' |∈| ta_der (fmap_states_ta CInl (ta 𝒜)) C⟨Var (CInl q'')⟩"
    by (auto simp: C_def) force
  from reach_fin have reach_fin: "CInl q' |∈| ta_der ?A C⟨Var (CInl q'')⟩"
    using Inl_A_res_Inf_automata[of "ta 𝒜" "C⟨Var (CInl q'')⟩"] by blast
  from lang(1) have fin: "CInr q' |∈| fin ?B" by (auto simp: Inf_reg_def)
  from reach_rule_st have reach: "q'' |∈| ta_der (ta 𝒜) (term_of_gterm (gsubt_at (gpair t u) p))"
    using ta_der_fmap_states_ta_mono2[of CInl] inj_CInl by (simp add: finj_CInl_CInr) blast
  have c: "fcard (𝒬 (ta 𝒜)) < depth (?none_t (gsubt_at u p))" using pos
    by (smt gposs_gsubst_at_subst_at_eq gposs_map_gterm le_trans not_le poss_append_poss poss_gposs_conv poss_length_bounded_by_depth)
  have "funas_term (?none_t (gsubt_at u p)) ⊆ (λ(f, n). ((None, Some f), n)) ` fset ℱ"
    using funas pos
    by (auto simp: funas_gterm_def, smt funas_term_ctxt_apply funas_term_of_gterm_conv
      gterm_to_None_Some_funas in_mono le_sup_iff subt_at_imp_ctxt term_of_gterm_gsubt)
  from this pigeonhole_ta_infinit_terms[OF c, of _ "λ t. t ⊆ (λ (f, n). ((None, Some f), n)) ` fset ℱ"]
  have "infinite {t. ground t ∧ q'' |∈| ta_der (ta 𝒜) t  ∧ funas_term t ⊆ (λ (f, n). ((None, Some f), n)) ` fset ℱ}"
    using reach by (auto simp: gp) (metis (mono_tags, lifting) Collect_cong) 
  then have "infinite {t. q'' |∈| ta_der (ta 𝒜) (term_of_gterm t) ∧ funas_gterm t ⊆ (λ(f, n). ((None, Some f), n)) ` fset ℱ}"
    using inf_ground_terms_to_gterms[of "λ t. q'' |∈| ta_der (ta 𝒜) t ∧ funas_term t ⊆ (λ (f, n). ((None, Some f), n)) ` fset ℱ"]
    by (auto simp: funas_term_of_gterm_conv)
  from infinite_set_dec_infinite[OF this, of gterm_to_None_Some "λ t. funas_gterm t ⊆ fset ℱ"]
  have "q'' |∈| Q_infty (ta 𝒜) ℱ" using funas_gterm_bot_some_decomp unfolding Q_infty_fmember
    by auto (smt Collect_cong funas_gterm_bot_some_decomp gterm_to_None_Some_funas)
  from res_rule_st_Inf_automata_dash rule_st this Inf_automata_reach_to_dash_reach[OF reach_fin]
  have "CInr q' |∈| ta_der (Inf_automata (ta 𝒜) (Q_infty (ta 𝒜) ℱ)) (term_of_gterm (gpair t u))"
    using gp_split gr_ctxt by (metis gp ground_ctxt_apply ground_term_of_gterm gterm_of_term_inv ta_der_ctxt)  
  then show ?thesis using fin by (auto simp: ℒ_def Inf_reg_def intro!: exI[of _ u] elim!: gta_langI)
qed

lemma CInr_Inf_automata_to_q_state:
  assumes "CInr p |∈| ta_der (Inf_automata 𝒜 Q) t" and "ground t"
  shows "∃ C s q. C⟨s⟩ = t ∧ CInr q |∈| ta_der (Inf_automata 𝒜 Q) s ∧ q |∈| Q ∧
    CInr p |∈| ta_der (Inf_automata 𝒜 Q) C⟨Var (CInr q)⟩ ∧
    (fst ∘ fst ∘ the ∘ root) s = None" using assms
proof (induct t arbitrary: p)
  case (Fun f ts)
  let ?A = "(Inf_automata 𝒜 Q)"
  from Fun(2) obtain qs q' where
    rule: "f qs → CInr q' |∈| rules ?A" "length qs = length ts" and
    eps: "q' = p ∨ (CInr q', CInr p) |∈| (eps ?A)|⇧+|" and
    reach: "∀ i < length ts. qs ! i |∈| ta_der ?A (ts ! i)"
    by auto (metis Inr_rhs_eps_Inr_lhs)
  consider (a) "⋀ i. i < length qs ⟹ ∃ q''. qs ! i = CInl q''" | (b) "∃ i < length qs. ∃ q''. qs ! i = CInr q''"
    by (meson remove_sum.cases)
  then show ?case
  proof cases
    case a
    then have "f qs → CInr q' |∈| |⋃| (q_inf_dash_intro_rules Q |`| rules 𝒜)" using rule
      by (auto simp: Inf_automata_def min_def upt_fset split!: if_splits)
         (smt Cons_nth_drop_Suc Inl_Inr_False append_Cons_nth_not_middle append_take_drop_id drop_map length_map local.rule(2) map_nth_eq_conv nth_append_length take_map)
    then show ?thesis using reach eps rule
      by (intro exI[of _ Hole] exI[of _ "Fun f ts"] exI[of _ q'])
         (auto split!: if_splits)
  next
    case b
    then obtain i q'' where b: "i < length ts" "qs ! i = CInr q''" using rule(2) by auto
    then have "CInr q'' |∈| ta_der ?A (ts ! i)" using rule(2) reach by auto 
    from Fun(3) Fun(1)[OF nth_mem, OF b(1) this] b rule(2) obtain C s q''' where
      ctxt: "C⟨s⟩ = ts ! i" and
      qinf: "CInr q''' |∈| ta_der (Inf_automata 𝒜 Q) s ∧ q''' |∈| Q" and
      reach2: "CInr q'' |∈| ta_der (Inf_automata 𝒜 Q) C⟨Var (CInr q''')⟩" and
      "(fst ∘ fst ∘ the ∘ root) s = None"
      by auto
    then show ?thesis using rule eps reach ctxt qinf reach2 b(1) b(2)[symmetric]
      by (auto simp: min_def nth_append_Cons simp flip: map_append id_take_nth_drop[OF b(1)]
        intro!: exI[of _ "More f (take i ts) C (drop (Suc i) ts)"] exI[of _ "s"] exI[of _ "q'''"] exI[of _ "CInr q'"] exI[of _ "qs"])
  qed
qed auto

lemma aux_lemma:
  assumes "RR2_spec 𝒜 ℛ" and "ℛ ⊆ {t. funas_gterm t ⊆ fset ℱ} × {t. funas_gterm t ⊆ fset ℱ}"
    and "infinite {u | u. gpair t u ∈ ℒ 𝒜}"
  shows "t ∈ Inf_branching_terms ℛ ℱ"
  using assms unfolding RR2_spec_def Inf_branching_terms_def
  apply (auto simp: ℒ_def)
  apply (smt Collect_cong SigmaD2 ℒ_def assms(3) gfst_gpair gsnd_gpair mem_Collect_eq subset_iff)
  by (smt RR2_spec_def SigmaD1 assms(1, 3) gpair_inject in_mono mem_Collect_eq not_finite_existsD)

lemma Inf_automata_to_Inf:
  assumes "RR2_spec 𝒜 ℛ"
    and "ℛ ⊆ {t. funas_gterm t ⊆ fset ℱ} × {t. funas_gterm t ⊆ fset ℱ}"
    and "gpair t u ∈ ℒ (Inf_reg 𝒜 (Q_infty (ta 𝒜) ℱ))"
  shows "t ∈ Inf_branching_terms ℛ ℱ"
proof -
  let ?g_to_term = "λ t. term_of_gterm t :: ('b, unit) term"
  let ?t_to_germ = "λ t. gterm_of_term t :: 'b gterm"
  let ?A = "Inf_automata (ta 𝒜) (Q_infty (ta 𝒜) ℱ)"
  from assms(3) obtain q where fin: "CInr q |∈| CInr |`| fin 𝒜" and
    reach_fin: "CInr q |∈| ta_der ?A (term_of_gterm (gpair t u))"
    by (auto simp: Inf_reg_def ℒ_def Inf_automata_def elim!: gta_langE)
  from CInr_Inf_automata_to_q_state[OF reach_fin] obtain C s p where
    ctxt: "C⟨s⟩ = term_of_gterm (gpair t u)" and
    q_inf_st: "CInr p |∈| ta_der ?A s" "p |∈| Q_infty (ta 𝒜) ℱ" and
    reach: "CInr q |∈| ta_der ?A C⟨Var (CInr p)⟩" and
    none: "(fst ∘ fst ∘ the ∘ root) s = None" by auto
  let ?C = "ctxt_of_pos_term (hole_pos C) (term_of_gterm u :: ('b, unit) term)"
  from ctxt have gr_ctxt: "ground_ctxt C" and gr_term: "ground s"
    by (metis ground_ctxt_apply ground_term_of_gterm)+
  {assume ass: "hole_pos C ∈ gposs t"
    then have "∃ f h. gfun_at (gpair t u) (hole_pos C) = Some (Some f, h)"
      using fun_at_gfun_at_conv poss_gposs_conv gfun_at_poss by auto
    moreover have "gfun_at (gpair t u) (hole_pos C) = fun_at C⟨s⟩ (hole_pos C)"
      using fun_at_gfun_at_conv ctxt by (metis hole_pos_poss poss_gposs_conv)
    ultimately have False using ctxt[symmetric] none by (cases s) (auto)}
  then have nt_pos_t [simp]: "hole_pos C ∉ gposs t" and pos_u [simp]: "hole_pos C ∈ gposs u"
    using ctxt by auto (metis gpair_poss_args_poss hole_pos_poss poss_gposs_conv)
  have  fun_gr_C': "ground_ctxt ?C" by auto
  from nt_pos_t pos_u ctxt have [simp]: "s = term_of_gterm (gterm_to_None_Some (gsubt_at u (hole_pos C)))"
    by (metis gr_term gsubt_at_ctxt_pos gterm_of_term_inv subst_at_gpair_nt_poss_None_Some term_of_gterm_inv)
  let ?S = "{t. funas_gterm t ⊆ fset ℱ ∧ p |∈| ta_der (ta 𝒜) (term_of_gterm (gterm_to_None_Some t))}"
  let ?S' = "{(gctxt_apply (ctxt_of_pos_term (hole_pos C) (term_of_gterm u)) w) | w.
    p |∈| ta_der (ta 𝒜) (term_of_gterm (gterm_to_None_Some w)) ∧ funas_gterm w ⊆ fset ℱ}"
  from infinite_inj_image_infinite have  "infinite (?g_to_term ` ?S)" using inj_term_of_gterm q_inf_st(2)
    by (auto simp: Q_infty_def)
  from infinite_inj_image_infinite[OF this, of "ctxt_apply_term (ctxt_of_pos_term (hole_pos C) (term_of_gterm u))"]
  have "infinite (ctxt_apply_term ?C ` ?g_to_term ` ?S)"
    by (meson ctxt_eq inj_onI)
  from infinite_inj_image_infinite[OF this] have "infinite (?t_to_germ ` ctxt_apply_term ?C ` ?g_to_term ` ?S)"
    using fun_gr_C' by (smt ground_ctxt_apply ground_term_of_gterm gterm_of_term_inj imageE)
  then have inf: "infinite ?S'" unfolding image_comp
    by (auto simp add: image_Collect) (smt Collect_cong finite_Collect_conjI) 
  {fix u assume "u ∈ ?S'" then obtain w where u: "u = gctxt_apply ?C w" and
      fun_r: "funas_gterm w ⊆ fset ℱ ∧ p |∈| ta_der (ta 𝒜) (term_of_gterm (gterm_to_None_Some w))"
      by (auto simp add: image_Collect image_comp)
    have conv: "gpair t (gctxt_apply ?C w) = gterm_of_term C⟨term_of_gterm (gterm_to_None_Some w)⟩" for w
      using ctxt[symmetric]
      by auto (metis gpair_ctxt_decomposition_2 gr_ctxt nt_pos_t term_of_gterm_inv) 
    from fun_r have "q |∈| ta_der (ta 𝒜) (term_of_gterm (gpair t u))" unfolding u conv
      using Inf_automata_dash_reach_to_reach[OF reach] gr_ctxt 
      by (auto simp: map_vars_term_ctxt_commute ground_ctxt_map_vars_to_adpat gterm_of_term_inv' adapt_vars_term_of_gterm ta_der_ctxt)
    then have "gpair t u ∈ ℒ 𝒜" using conjunct1[OF fun_r] fin
      by (auto simp: ℒ_def Inf_automata_def gta_langI)}
  from this infinite_set_restrict_to_property[OF _ inf, of "λ u. gpair t u ∈ ℒ 𝒜"]
  have "infinite {u. gpair t u ∈ ℒ 𝒜}" by auto
  from aux_lemma[OF assms(1, 2), of t] this show ?thesis by auto
qed

end