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 Cs = 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  " "Cs = t'" "C2v = s" and
    loop: "p |∈| ta_der 𝒜 v" "p |∈| ta_der 𝒜 C2Var p" "q |∈| ta_der 𝒜 CVar 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) CVar (CInl q)"
  shows "CInr p |∈| ta_der (Inf_automata 𝒜 Q) CVar (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 @ CVar (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) CVar (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. Cs = t  CInr q |∈| ta_der (Inf_automata 𝒜 Q) s  q |∈| Q 
    CInr p |∈| ta_der (Inf_automata 𝒜 Q) CVar (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: "Cs = ts ! i" and
      qinf: "CInr q''' |∈| ta_der (Inf_automata 𝒜 Q) s  q''' |∈| Q" and
      reach2: "CInr q'' |∈| ta_der (Inf_automata 𝒜 Q) CVar (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: "Cs = 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 CVar (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 vG}"
    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 Cs) (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))vG = (gctxt_of_ctxt C)gterm_to_None_Some vG" 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))vG)   𝒜}" 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