Theory Regular_Tree_Relations.RR2_Infinite

theory RR2_Infinite
  imports RRn_Automata Tree_Automata_Pumping
begin


lemma map_ta_rule_id [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 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.n_lists n L)) 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.n_lists (length ts) L))" using L(1)
      by (auto simp: image_iff set_n_lists)
    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_imageD:
  "infinite (f ` S) ⟹ inj_on f S ⟹ infinite S"
  by blast

lemma infinite_imageD2:
  "infinite (f ` S) ⟹ inj f ⟹ infinite S"
  by blast

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

(*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 depth_gterm_conv:
  "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

lemma pigeonhole_ta_infinit_terms:
  fixes t ::"'f gterm" and 𝒜 :: "('q, 'f) ta"
  defines "t' ≡ term_of_gterm t :: ('f, 'q) term"
  assumes "fcard (𝒬 𝒜) < depth t'" and "q |∈| gta_der 𝒜 t" and "P (funas_gterm t)"
  shows "infinite {t . q |∈| gta_der 𝒜 t ∧ P (funas_gterm t)}"
proof -
  from pigeonhole_tree_automata[OF _ assms(3)[unfolded gta_der_def]] assms(2,4)
  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⟩"
    unfolding assms(1) by auto
  let ?terms = "λ n. C⟨(C2 ^n)⟨v⟩⟩" let ?inner = "λ n. (C2 ^n)⟨v⟩"
  have gr: "ground_ctxt C2" "ground_ctxt C" "ground v"
    using arg_cong[OF ctxt(2), of ground] unfolding ctxt(3)[symmetric] assms(1)
    by fastforce+
  moreover have funas: "funas_term (?terms (Suc n)) = funas_term t'" for n
    unfolding ctxt(2, 3)[symmetric] using ctxt_comp_n_pres_funas by auto
  moreover have der: "q |∈| ta_der 𝒜 (?terms (Suc n))" for n using loop
    by (meson ta_der_ctxt ta_der_ctxt_n_loop)
  moreover have "n < depth (?terms (Suc n))" for n
    by (meson ctxt(1) ctxt_comp_n_lower_bound depth_ctxt_less_eq less_le_trans)
  ultimately have "q |∈| ta_der 𝒜 (?terms (Suc n)) ∧ ground (?terms (Suc n)) ∧
    P (funas_term (?terms (Suc n))) ∧ n < depth (?terms (Suc n))" for n using assms(4)
    by (auto simp: assms(1) funas_term_of_gterm_conv)
  then have inf: "infinite {t. q |∈| ta_der 𝒜 t ∧ ground t ∧ P (funas_term t)}"
    by (intro no_upper_bound_infinite[of _ depth]) blast
  have inj: "inj_on gterm_of_term {t. q |∈| ta_der 𝒜 t ∧ ground t ∧ P (funas_term t)}"
    by (intro gterm_of_term_inj) simp
  show ?thesis
    by (intro infinite_super[OF _ infinite_inj_image_infinite[OF inf inj]])
       (auto simp: image_def gta_der_def funas_gterm_gterm_of_term)
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 ∧ funas_gterm t ⊆ ℱ" using assms
proof (induct s)
  case (GFun f ts)
  from GFun(1)[OF nth_mem] obtain ss where l: "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 have "i < length ss ⟹ funas_gterm (ss ! i) ⊆ ℱ" for i using GFun(2)
    by (auto simp: UN_subset_iff) (smt (z3) gterm_to_None_Some_funas nth_mem subsetD)
  then show ?case using GFun(2-) l
    by (cases f) (force simp: map_nth_eq_conv UN_subset_iff dest!: in_set_idx intro!: exI[of _ "GFun (the (snd f)) ss"])
qed

(* Definition INF, Q_infinity and automata construction *)

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

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 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 𝒜)|⇧+|"
  by (intro ftrancl_map_both_fsubset) (auto simp: finj_CInl_CInr)

lemma map_both_CInr_ftrancl_conv:
  "(map_both CInr |`| eps 𝒜)|⇧+| = map_both CInr |`| (eps 𝒜)|⇧+|"
  by (intro ftrancl_map_both_fsubset) (auto simp: finj_CInl_CInr)

lemmas map_both_ftrancl_conv = map_both_CInl_ftrancl_conv map_both_CInr_ftrancl_conv 

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: map_both_ftrancl_conv dest: 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 ftrancl_map_both_fsubset[OF finj_CInl_CInr(1)]
  by (cases q) (auto simp: Inf_automata_def map_both_ftrancl_conv)

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 map_both_ftrancl_conv)

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"
proof (rule ta_der_mono)
  show "rules (fmap_states_ta CInl 𝒜) |⊆| rules (Inf_automata 𝒜 Q)"
    apply (rule fsubsetI)
    by (auto simp: Inf_automata_def fmap_states_ta_def' image_iff Bex_def)
next
  show "eps (fmap_states_ta CInl 𝒜) |⊆| eps (Inf_automata 𝒜 Q)"
    by (rule fsubsetI) (simp add: Inf_automata_def fmap_states_ta_def')
qed

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
  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: 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 Inf_automata_dashI:
  assumes "run 𝒜 r (gterm_to_None_Some t)" and "ex_rule_state r |∈| Q"
  shows "CInr (ex_rule_state r) |∈| gta_der (Inf_automata 𝒜 Q) (gterm_to_None_Some t)"
proof (cases t)
  case [simp]: (GFun f ts)
  from run_root_rule[OF assms(1)] run_argsD[OF assms(1)] have
    rule: "TA_rule (None, Some f) (map ex_comp_state (gargs r)) (ex_rule_state r) |∈| rules 𝒜" "length (gargs r) = length ts" and
    reach: "∀ i < length ts. ex_comp_state (gargs r ! i) |∈| ta_der 𝒜 (term_of_gterm (gterm_to_None_Some (ts  ! i)))"
    by (auto intro!: run_to_comp_st_gta_der[unfolded gta_der_def comp_def])
  from rule assms(2) have "(None, Some f) (map (CInl ∘ ex_comp_state) (gargs r)) → CInr (ex_rule_state r) |∈| rules  (Inf_automata 𝒜 Q)"
    apply (simp add: Inf_automata_def image_iff bex_Un)
    apply (rule disjI1)
    by 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 simp: gta_der_def intro!: exI[of _ "CInr (ex_rule_state r)"]  exI[of _ "map (CInl ∘ ex_comp_state) (gargs r)"])
        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: Inf_automata_def ftrancl_map_both map_both_ftrancl_conv)
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
  from assms dt p(2, 3) have "length (take (Suc m') p) = Suc m'"
    by (metis Suc_leI depth_gterm_conv length_take less_add_Suc1 less_imp_le_nat less_le_trans min.absorb2)
  then have nt: "take (Suc m') p ∉ gposs t" using poss_length_bounded_by_depth dt depth_gterm_conv
    by (metis Suc_n_not_le_n gposs_to_poss)
  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 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"
  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" "p ∉ gposs t" and card: "fcard (𝒬 (ta 𝒜)) < length q" by auto
  then have gp: "gsubt_at (gpair t u) p = gterm_to_None_Some (gsubt_at u p)"
    using subst_at_gpair_nt_poss_None_Some[of p] by force
  from lang obtain r where r: "run (ta 𝒜) r (gpair t u)" "ex_comp_state r |∈| fin 𝒜"
    unfolding ℒ_def gta_lang_def by (fastforce dest: gta_der_to_run)
  from pos have p_gtu: "p ∈ gposs (gpair t u)" and pu: "p ∈ gposs u"
    using not_gposs_append by auto
  have qinf: "ex_rule_state (gsubt_at r p) |∈| Q_infty (ta 𝒜) ℱ"
    using funas_gterm_gsubt_at_subseteq[OF pu] funas card
    unfolding Q_infty_fmember gta_der_def[symmetric]
    by (intro infinite_super[THEN infinite_imageD2[OF _ inj_gterm_to_None_Some],
     OF _ pigeonhole_ta_infinit_terms[of "ta 𝒜" "gsubt_at (gpair t u) p" _
     "λ t. t ⊆ (λ(f, n). ((None, Some f), n)) ` fset ℱ",
     OF _ run_to_gta_der_gsubt_at(1)[OF r(1) p_gtu]]])
        (auto simp: poss_length_bounded_by_depth[of q] image_iff gp less_le_trans
                   pos(1) poss_gposs_conv pu dest!: funas_gterm_bot_some_decomp)
  from Inf_automata_dashI[OF run_gsubt_cl[OF r(1) p_gtu, unfolded gp] qinf]
  have dashI: "CInr (ex_rule_state (gsubt_at r p)) |∈| gta_der (Inf_automata (ta 𝒜) (Q_infty (ta 𝒜) ℱ)) (gsubt_at (gpair t u) p)"
    unfolding gp[symmetric] .
  have "CInl (ex_comp_state r) |∈| ta_der ?A (ctxt_at_pos (term_of_gterm (gpair t u)) p)⟨Var (CInl (ex_rule_state (gsubt_at r p)))⟩"
    using ta_der_fmap_states_ta[OF run_ta_der_ctxt_split2[OF r(1) p_gtu], of CInl, THEN fsubsetD[OF Inl_A_res_Inf_automata]]
    unfolding replace_term_at_replace_at_conv[OF gposs_to_poss[OF p_gtu]]
    by (auto simp: gterm.map_ident simp flip: map_term_replace_at_dist[OF gposs_to_poss[OF p_gtu]])
  from ta_der_ctxt[OF dashI[unfolded gta_der_def] Inf_automata_reach_to_dash_reach[OF this]]
  have "CInr (ex_comp_state r) |∈| gta_der (Inf_automata (ta 𝒜) (Q_infty (ta 𝒜) ℱ)) (gpair t u)"
    unfolding replace_term_at_replace_at_conv[OF gposs_to_poss[OF p_gtu]]
    unfolding replace_gterm_conv[OF p_gtu]
    by (auto simp: gta_der_def)
  moreover from r(2) have "CInr (ex_comp_state r) |∈| fin (Inf_reg 𝒜 (Q_infty (ta 𝒜) ℱ))"
    by (auto simp: Inf_reg_def)
  ultimately show ?thesis using r(2)
    by (auto simp: ℒ_def gta_der_def Inf_reg_def intro: exI[of _ u])
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)
         (metis (no_types, lifting) Inl_Inr_False Suc_pred append_eq_append_conv id_take_nth_drop
               length_Cons length_drop length_greater_0_conv length_map
               less_nat_zero_code list.size(3) nth_append_length rule(2))
   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 "ℛ ⊆ 𝒯⇩G (fset ℱ) × 𝒯⇩G (fset ℱ)"
    and "infinite {u | u. gpair t u ∈ ℒ 𝒜}"
  shows "t ∈ Inf_branching_terms ℛ ℱ"
proof -
  from assms have [simp]: "gpair t u ∈ ℒ 𝒜 ⟷ (t, u) ∈ ℛ ∧ u ∈ 𝒯⇩G (fset ℱ)"
    for u by (auto simp: RR2_spec_def)
  from assms have "t ∈ 𝒯⇩G (fset ℱ)" unfolding RR2_spec_def
    by (auto dest: not_finite_existsD)
  then show ?thesis using assms unfolding Inf_branching_terms_def
    by (auto simp: 𝒯⇩G_equivalent_def)
qed

lemma Inf_automata_to_Inf:
  assumes "RR2_spec 𝒜 ℛ" and "ℛ ⊆ 𝒯⇩G (fset ℱ) × 𝒯⇩G (fset ℱ)"
    and "gpair t u ∈ ℒ (Inf_reg 𝒜 (Q_infty (ta 𝒜) ℱ))"
  shows "t ∈ Inf_branching_terms ℛ ℱ"
proof -
  let ?con = "λ t. term_of_gterm (gterm_to_None_Some t)"
  let ?A = "Inf_automata (ta 𝒜) (Q_infty (ta 𝒜) ℱ)"
  from assms(3) obtain q where fin: "q |∈| 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
  have gr: "ground s" "ground_ctxt C" using arg_cong[OF ctxt, of ground]
    by auto
  have reach: "q |∈| ta_der (ta 𝒜) (adapt_vars_ctxt C)⟨Var p⟩"
    using gr Inf_automata_dash_reach_to_reach[OF reach]
    by (auto simp: map_vars_term_ctxt_apply)
  from q_inf_st(2) have inf: "infinite {v. funas_gterm v ⊆ fset ℱ ∧ p |∈| ta_der (ta 𝒜) (?con v)}"
    by (simp add: Q_infty_fmember)
  have inf: "infinite {v. funas_gterm v ⊆ fset ℱ ∧ q |∈| gta_der (ta 𝒜) (gctxt_of_ctxt C)⟨gterm_to_None_Some v⟩⇩G}"
    using reach ground_ctxt_adapt_ground[OF gr(2)] gr
    by (intro infinite_super[OF _ inf], auto simp: gta_der_def)
       (smt (z3) adapt_vars_ctxt adapt_vars_term_of_gterm ground_gctxt_of_ctxt_apply_gterm ta_der_ctxt)
  have *: "gfun_at (gterm_of_term C⟨s⟩) (hole_pos C) = gfun_at (gterm_of_term s) []"
    by (induct C) (auto simp: nth_append_Cons)
  from arg_cong[OF ctxt, of "λ t. gfun_at (gterm_of_term t) (hole_pos C)"] none
  have hp_nt: "ghole_pos (gctxt_of_ctxt C) ∉ gposs t" unfolding ground_hole_pos_to_ghole[OF gr(2)]
    using gfun_at_gpair[of t u "hole_pos C"] gr *
    by (cases s) (auto simp flip: poss_gposs_mem_conv split: if_splits elim: gfun_at_possE)
  from gpair_ctxt_decomposition[OF hp_nt, of u "gsubt_at u (hole_pos C)"]
  have to_gpair: "gpair t (gctxt_at_pos u (hole_pos C))⟨v⟩⇩G = (gctxt_of_ctxt C)⟨gterm_to_None_Some v⟩⇩G" for v
    unfolding ground_hole_pos_to_ghole[OF gr(2)] using ctxt gr
    using subst_at_gpair_nt_poss_None_Some[OF _ hp_nt, of u]
    by (metis (no_types, lifting) UnE ‹ghole_pos (gctxt_of_ctxt C) = hole_pos C›
        gposs_of_gpair gsubt_at_gctxt_apply_ghole hole_pos_in_ctxt_apply hp_nt poss_gposs_conv term_of_gterm_ctxt_apply)
  have inf: "infinite {v. gpair t ((gctxt_at_pos u (hole_pos C))⟨v⟩⇩G) ∈ ℒ 𝒜}" using fin
    by (intro infinite_super[OF _ inf]) (auto simp: ℒ_def gta_der_def simp flip: to_gpair)
  have "infinite {u |u. gpair t u ∈ ℒ 𝒜}"
    by (intro infinite_super[OF _ infinite_inj_image_infinite[OF inf gctxt_apply_inj_on_term[of "gctxt_at_pos u (hole_pos C)"]]])
       (auto simp: image_def intro: infinite_super)
  then show ?thesis using assms(1, 2)
    by (intro aux_lemma[of 𝒜]) simp
qed

lemma Inf_automata_subseteq:
  "ℒ (Inf_reg 𝒜 (Q_infty (ta 𝒜) ℱ)) ⊆ ℒ 𝒜" (is "ℒ ?IA ⊆ _")
proof
  fix s assume l: "s ∈ ℒ ?IA"
  then obtain q where w: "q |∈| fin ?IA" "q |∈| ta_der (ta ?IA) (term_of_gterm s)"
    by (auto simp: ℒ_def elim!: gta_langE)
  from w(1) have "remove_sum q |∈| fin 𝒜"
    by (auto simp: Inf_reg_def Inf_automata_def)
  then show "s ∈ ℒ 𝒜" using Inf_automata_dash_reach_to_reach[of q "ta 𝒜"] w(2)
    by (auto simp: gterm.map_ident ℒ_def Inf_reg_def)
       (metis gta_langI map_vars_term_term_of_gterm)
qed

lemma ℒ_Inf_reg:
  assumes "RR2_spec 𝒜 ℛ" and "ℛ ⊆ 𝒯⇩G (fset ℱ) × 𝒯⇩G (fset ℱ)"
  shows "gfst ` ℒ (Inf_reg 𝒜 (Q_infty (ta 𝒜) ℱ)) = Inf_branching_terms ℛ ℱ"
proof -
  {fix s assume ass: "s ∈ ℒ (Inf_reg 𝒜 (Q_infty (ta 𝒜) ℱ))"
    then have "∃ t u. s = gpair t u" using Inf_automata_subseteq[of 𝒜 ℱ] assms(1)
      by (auto simp: RR2_spec_def)
    then have "gfst s ∈ Inf_branching_terms ℛ ℱ"
      using ass Inf_automata_to_Inf[OF assms]
      by (force simp: gfst_gpair)}
  then show ?thesis using Inf_to_automata[OF assms(1), of _ ℱ]
    by (auto simp: gfst_gpair) (metis gfst_gpair image_iff)
qed
end