# 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'"
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)}"
have inf: "infinite {v. funas_gterm v ⊆ fset ℱ ∧ q |∈| gta_der (ta 𝒜) (gctxt_of_ctxt C)⟨gterm_to_None_Some v⟩⇩G}"
by (intro infinite_super[OF _ inf], auto simp: gta_der_def)
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```