Theory Regular_Tree_Relations.RR2_Infinite_Q_infinity

theory RR2_Infinite_Q_infinity
  imports RR2_Infinite
begin

(* This section constructs an executable membership check for Q infinity,
  since Inf_automata is already executable (for all sets Q where checking membership is executable)
*)

lemma if_cong':
  "b = c  x = u  y = v  (if b then x else y) = (if c then u else v)"
  by auto

(* The reachable terms where eps transitions can only occur after the rule *)
fun ta_der_strict :: "('q,'f) ta  ('f,'q) term  'q fset" where
  "ta_der_strict 𝒜 (Var q) = {|q|}"
| "ta_der_strict 𝒜 (Fun f ts) = {| q' | q' q qs. TA_rule f qs q |∈| rules 𝒜  (q = q'  (q, q') |∈| (eps 𝒜)|+|)  
    length qs = length ts  ( i < length ts. qs ! i |∈| ta_der_strict 𝒜 (ts ! i))|}"

lemma ta_der_strict_Var:
  "q |∈| ta_der_strict 𝒜 (Var x)  x = q"
  unfolding ta_der.simps by auto

lemma ta_der_strict_Fun:
  "q |∈| ta_der_strict 𝒜 (Fun f ts)  ( ps p. TA_rule f ps p |∈| (rules 𝒜) 
      (p = q  (p, q) |∈| (eps 𝒜)|+|)  length ps = length ts  
      ( i < length ts. ps ! i |∈| ta_der_strict 𝒜 (ts ! i)))" (is "?Ls  ?Rs")
  unfolding ta_der_strict.simps
  by (intro iffI fCollect_memberI finite_Collect_less_eq[OF _ finite_eps[of 𝒜]]) auto

declare ta_der_strict.simps[simp del]
lemmas ta_der_strict_simps [simp] = ta_der_strict_Var ta_der_strict_Fun

lemma ta_der_strict_sub_ta_der:
  "ta_der_strict 𝒜 t |⊆| ta_der 𝒜 t"
proof (induct t)
  case (Fun f ts)
  then show ?case
    by auto (metis fsubsetD nth_mem)+
qed auto
  
lemma ta_der_strict_ta_der_eq_on_ground:
  assumes"ground t"
  shows "ta_der 𝒜 t = ta_der_strict 𝒜 t"
proof
  {fix q assume "q |∈| ta_der 𝒜 t" then have "q |∈| ta_der_strict 𝒜 t" using assms
    proof (induct t arbitrary: q)
      case (Fun f ts)
      then show ?case apply auto
        using nth_mem by blast+
    qed auto}
  then show "ta_der 𝒜 t |⊆| ta_der_strict 𝒜 t"
    by auto
next
  show "ta_der_strict 𝒜 t |⊆| ta_der 𝒜 t" using ta_der_strict_sub_ta_der .
qed

lemma ta_der_to_ta_strict:
  assumes "q |∈| ta_der A CVar p" and "ground_ctxt C"
  shows " q'. (p = q'  (p, q') |∈| (eps A)|+|)  q |∈| ta_der_strict A CVar q'"
  using assms
proof (induct C arbitrary: q p)
  case (More f ss C ts)
  from More(2) obtain qs q' where
    r: "TA_rule f qs q' |∈| rules A" "length qs = Suc (length ss + length ts)" "q' = q  (q', q) |∈| (eps A)|+|" and
    rec: " i < length qs. qs ! i |∈| ta_der A ((ss @ CVar p # ts) ! i)"
    by auto
  from More(1)[of "qs ! length ss" p] More(3) rec r(2) obtain q'' where
    mid: "(p = q''  (p, q'') |∈| (eps A)|+|)  qs ! length ss |∈| ta_der_strict A CVar q''"
    by auto (metis length_map less_add_Suc1 nth_append_length)
  then have " i < length qs. qs ! i |∈| ta_der_strict A ((ss @ CVar q'' # ts) ! i)"
    using rec r(2) More(3)
    using ta_der_strict_ta_der_eq_on_ground[of _ A]
    by (auto simp: nth_append_Cons all_Suc_conv split:if_splits cong: if_cong')
  then show ?case using rec r conjunct1[OF mid]
    by (rule_tac x = q'' in exI, auto intro!: exI[of _ q'] exI[of _ qs])
qed auto

fun root_ctxt where
  "root_ctxt (More f ss C ts) = f"
| "root_ctxt  = undefined"

lemma root_to_root_ctxt [simp]:
  assumes "C  "
  shows "fst (the (root Ct))  root_ctxt C"
  using assms by (cases C) auto


(* Q_inf section *)

inductive_set Q_inf for 𝒜 where
  trans: "(p, q)  Q_inf 𝒜  (q, r)  Q_inf 𝒜  (p, r)  Q_inf 𝒜"
| rule: "(None, Some f) qs  q |∈| rules 𝒜  i < length qs  (qs ! i, q)  Q_inf 𝒜"
| eps: "(p, q)  Q_inf 𝒜  (q, r) |∈| eps 𝒜  (p, r)  Q_inf 𝒜"

abbreviation "Q_inf_e 𝒜  {q | p q. (p, p)  Q_inf 𝒜  (p, q)  Q_inf 𝒜}"

lemma Q_inf_states_ta_states:
  assumes "(p, q)  Q_inf 𝒜"
  shows "p |∈| 𝒬 𝒜" "q |∈| 𝒬 𝒜"
  using assms by (induct) (auto simp: rule_statesD eps_statesD)

lemma Q_inf_finite:
  "finite (Q_inf 𝒜)" "finite (Q_inf_e 𝒜)"
proof -
  have *: "Q_inf 𝒜  fset (𝒬 𝒜 |×| 𝒬 𝒜)" "Q_inf_e 𝒜  fset (𝒬 𝒜)"
    by (auto simp add: Q_inf_states_ta_states(1, 2) subrelI)
  show "finite (Q_inf 𝒜)"
    by (intro finite_subset[OF *(1)]) simp
  show "finite (Q_inf_e 𝒜)"
    by (intro finite_subset[OF *(2)]) simp
qed

context
includes fset.lifting
begin
lift_definition fQ_inf :: "('a, 'b option × 'c option) ta  ('a × 'a) fset" is Q_inf
  by (simp add: Q_inf_finite(1))
lift_definition fQ_inf_e :: "('a, 'b option × 'c option) ta  'a fset" is Q_inf_e
  using Q_inf_finite(2) .
end


lemma Q_inf_ta_eps_Q_inf:
  assumes "(p, q)  Q_inf 𝒜" and "(q, q') |∈| (eps 𝒜)|+|"
  shows "(p, q')  Q_inf 𝒜" using assms(2, 1)
  by (induct rule: ftrancl_induct) (auto simp add: Q_inf.eps)

lemma lhs_state_rule:
  assumes "(p, q)  Q_inf 𝒜"
  shows " f qs r. (None, Some f) qs  r |∈| rules 𝒜  p |∈| fset_of_list qs"
  using assms by induct (force intro: nth_mem)+

lemma Q_inf_reach_state_rule:
  assumes "(p, q)  Q_inf 𝒜" and "𝒬 𝒜 |⊆| ta_reachable 𝒜"
  shows " ss ts f C. q |∈| ta_der 𝒜 (More (None, Some f) ss C ts)Var p  ground_ctxt (More (None, Some f) ss C ts)"
    (is " ss ts f C. ?P ss ts f C q p")
  using assms
proof (induct)
  case (trans p q r)
  then obtain f1 f2 ss1 ts1 ss2 ts2 C1 C2 where
    C: "?P ss1 ts1 f1 C1 q p" "?P ss2 ts2 f2 C2 r q" by blast
  then show ?case
    apply (rule_tac x = "ss2" in exI, rule_tac x = "ts2" in exI, rule_tac x = "f2" in exI,
        rule_tac x = "C2 c (More (None, Some f1) ss1 C1 ts1)" in exI)
    apply (auto simp del: ctxt_apply_term.simps)
    apply (metis Subterm_and_Context.ctxt_ctxt_compose ctxt_compose.simps(2) ta_der_ctxt)
    done
next
  case (rule f qs q i)
  have " i < length qs.  t. qs ! i |∈| ta_der 𝒜 t  ground t"
    using rule(1, 2) fset_mp[OF rule(3), of "qs ! i" for i]
    by auto (meson fnth_mem rule_statesD(4) ta_reachableE) 
  then obtain ts where wit: "length ts = length qs"
    " i < length qs. qs ! i |∈| ta_der 𝒜 (ts ! i)  ground (ts ! i)"
    using Ex_list_of_length_P[of "length qs" "λ x i. qs ! i |∈| ta_der 𝒜 x  ground x"] by blast
  {fix j assume "j < length qs"
    then have "qs ! j |∈| ta_der 𝒜 ((take i ts @ Var (qs ! i) # drop (Suc i) ts) ! j)"
      using wit by (cases "j < i") (auto simp: min_def nth_append_Cons)}
  then have " i < length qs. qs ! i |∈| (map (ta_der 𝒜) (take i ts @ Var (qs ! i) # drop (Suc i) ts)) ! i"
    using wit rule(2) by (auto simp: nth_append_Cons)
  then have res: "q |∈| ta_der 𝒜 (Fun (None, Some f) (take i ts @ Var (qs ! i) # drop (Suc i) ts))"
    using rule(1, 2) wit by (auto simp: min_def nth_append_Cons intro!: exI[of _ q] exI[of _ qs])
  then show ?case using rule(1, 2) wit
    apply (rule_tac x = "take i ts" in exI, rule_tac x = "drop (Suc i) ts" in exI)
    apply (auto simp: take_map drop_map  dest!: in_set_takeD in_set_dropD simp del: ta_der_simps intro!: exI[of _ f] exI[of _ Hole])
    apply (metis all_nth_imp_all_set)+
    done
next
  case (eps p q r)
  then show ?case by (meson r_into_rtrancl ta_der_eps)
qed

lemma rule_target_Q_inf:
  assumes "(None, Some f) qs  q' |∈| rules 𝒜" and "i < length qs"
   shows "(qs ! i, q')  Q_inf 𝒜" using assms  
  by (intro rule) auto

lemma rule_target_eps_Q_inf:
  assumes "(None, Some f) qs  q' |∈| rules 𝒜" "(q', q) |∈| (eps 𝒜)|+|"
     and "i < length qs"
   shows "(qs ! i, q)  Q_inf 𝒜"
  using assms(2, 1, 3) by (induct rule: ftrancl_induct) (auto intro: rule eps)


lemma step_in_Q_inf:
  assumes "q |∈| ta_der_strict 𝒜 (map_funs_term (λf. (None, Some f)) (Fun f (ss @ Var p # ts)))"
    shows "(p, q)  Q_inf 𝒜"
  using assms rule_target_eps_Q_inf[of f _ _ 𝒜 q] rule_target_Q_inf[of f _ q 𝒜]
  by (auto simp: comp_def nth_append_Cons split!: if_splits) 


lemma ta_der_Q_inf:
  assumes "q |∈| ta_der_strict 𝒜 (map_funs_term (λf. (None, Some f)) (CVar p))" and "C  Hole"
  shows "(p, q)  Q_inf 𝒜" using assms
proof (induct C arbitrary: q)
  case (More f ss C ts)
  then show ?case
  proof (cases "C = Hole")
    case True
    then show ?thesis using More(2) by (auto simp: step_in_Q_inf)
  next
    case False
    then obtain q' where q: "q' |∈| ta_der_strict 𝒜 (map_funs_term (λf. (None, Some f)) CVar p)"
     "q |∈| ta_der_strict 𝒜 (map_funs_term (λf. (None, Some f)) (Fun f (ss @ Var q' # ts)))"
      using More(2) length_map
     (* SLOW *)
      by (auto simp: comp_def nth_append_Cons split: if_splits cong: if_cong')
         (smt nat_neq_iff nth_map ta_der_strict_simps)+
    have "(p, q')  Q_inf 𝒜" using More(1)[OF q(1) False] .
    then show ?thesis using step_in_Q_inf[OF q(2)] by (auto intro: trans)
  qed
qed auto

lemma Q_inf_e_infinite_terms_res:
  assumes "q  Q_inf_e 𝒜" and "𝒬 𝒜 |⊆| ta_reachable 𝒜"
  shows "infinite {t. q |∈| ta_der 𝒜 (term_of_gterm t)  fst (groot_sym t) = None}"
proof -
  let ?P ="λ u. ground u  q |∈| ta_der 𝒜 u  fst (fst (the (root u))) = None"
  have groot[simp]: "fst (fst (the (root (term_of_gterm t)))) = fst (groot_sym t)" for t by (cases t) auto
  have [simp]: "C    fst (fst (the (root Ct))) = fst (root_ctxt C)" for C t by (cases C) auto
  from assms(1) obtain p where cycle: "(p, p)  Q_inf 𝒜" "(p, q)  Q_inf 𝒜" by auto
  from Q_inf_reach_state_rule[OF cycle(1) assms(2)] obtain C where
    ctxt: "C  " "ground_ctxt C" and reach: "p |∈| ta_der 𝒜 CVar p"
    by blast
  obtain C2 where
    closing_ctxt: "C2  " "ground_ctxt C2" "fst (root_ctxt C2) = None" and cl_reach: "q |∈| ta_der 𝒜 C2Var p"
    by (metis (full_types) Q_inf_reach_state_rule[OF cycle(2) assms(2)] ctxt.distinct(1) fst_conv root_ctxt.simps(1))
  from assms(2) obtain t where t: "p |∈| ta_der 𝒜 t" and gr_t: "ground t"
    by (meson Q_inf_states_ta_states(1) cycle(1) fsubsetD ta_reachableE)
  let ?terms = "λ n. (C ^ Suc n)t" let ?S = "{?terms n | n. p |∈| ta_der 𝒜 (?terms n)  ground (?terms n)}"
  have "ground (?terms n)" for n using ctxt(2) gr_t by auto
  moreover have "p |∈| ta_der 𝒜 (?terms n)" for n using reach t(1)
    by (auto simp: ta_der_ctxt) (meson ta_der_ctxt ta_der_ctxt_n_loop)
  ultimately have inf: "infinite ?S" using ctxt_comp_n_lower_bound[OF ctxt(1)]
    using no_upper_bound_infinite[of _ depth, of ?S] by blast
  from infinite_inj_image_infinite[OF this] have inf:"infinite (ctxt_apply_term C2 ` ?S)"
    by (smt ctxt_eq inj_on_def)
  {fix u assume "u  (ctxt_apply_term C2 ` ?S)"
    then have "?P u" unfolding image_Collect using closing_ctxt cl_reach
      by (auto simp: ta_der_ctxt)}
  from this have inf: "infinite {u. ground u  q |∈| ta_der 𝒜 u  fst (fst (the (root u))) = None}"
    by (intro infinite_super[OF _ inf] subsetI) fast
  have inf: "infinite (gterm_of_term ` {u. ground u  q |∈| ta_der 𝒜 u  fst (fst (the (root u))) = None})"
    by (intro infinite_inj_image_infinite[OF inf] gterm_of_term_inj) auto
  show ?thesis
    by (intro infinite_super[OF _ inf]) (auto dest: groot_sym_gterm_of_term)
qed













lemma gfun_at_after_hole_pos:
  assumes "ghole_pos C p p"
  shows "gfun_at CtG p = gfun_at t (p -p ghole_pos C)" using assms
proof (induct C arbitrary: p)
  case (GMore f ss C ts) then show ?case
    by (cases p) auto
qed auto

lemma pos_diff_0 [simp]: "p -p p = []"
  by (auto simp: pos_diff_def)

lemma Max_suffI: "finite A  A = B  Max A = Max B"
  by (intro Max_eq_if) auto

lemma nth_args_depth_eqI:
  assumes "length ss = length ts"
    and " i. i < length ts  depth (ss ! i) = depth (ts ! i)"
  shows "depth (Fun f ss) = depth (Fun g ts)"
proof -
  from assms(1, 2) have "depth ` set ss = depth ` set ts"
    using nth_map_conv[OF assms(1), of depth depth]
    by (simp flip: set_map)
  from Max_suffI[OF _ this] show ?thesis using assms(1)
    by (cases ss; cases ts) auto
qed

lemma subt_at_ctxt_apply_hole_pos [simp]: "Cs |_ hole_pos C = s"
  by (induct C) auto

lemma ctxt_at_pos_ctxt_apply_hole_poss [simp]: "ctxt_at_pos Cs (hole_pos C) = C"
  by (induct C) auto

abbreviation "map_funs_ctxt f  map_ctxt f (λ x. x)"
lemma map_funs_term_ctxt_apply [simp]:
  "map_funs_term f Cs = (map_funs_ctxt f C)map_funs_term f s"
  by (induct C) auto

lemma map_funs_term_ctxt_decomp:
  assumes "map_funs_term fg t = Cs"
  shows " D u. C = map_funs_ctxt fg D  s = map_funs_term fg u  t = Du"
using assms
proof (induct C arbitrary: t)
  case Hole
  show ?case
    by (rule exI[of _ Hole], rule exI[of _ t], insert Hole, auto)
next
  case (More g bef C aft)
  from More(2) obtain f ts where t: "t = Fun f ts" by (cases t, auto)
  from More(2)[unfolded t] have f: "fg f = g" and ts: "map (map_funs_term fg) ts = bef @ Cs # aft" (is "?ts = ?bca") by auto
  from ts have "length ?ts = length ?bca" by auto
  then have len: "length ts = length ?bca" by auto
  note id = ts[unfolded map_nth_eq_conv[OF len], THEN spec, THEN mp]
  let ?i = "length bef"
  from len have i: "?i < length ts" by auto
  from id[of ?i] have "map_funs_term fg (ts ! ?i) = Cs" by auto
  from More(1)[OF this] obtain D u where D: "C = map_funs_ctxt fg D" and
    u: "s = map_funs_term fg u" and id: "ts ! ?i = Du" by auto
  from ts have "take ?i ?ts = take ?i ?bca" by simp
  also have "... = bef" by simp
  finally have bef: "map (map_funs_term fg) (take ?i ts) = bef" by (simp add: take_map)
  from ts have "drop (Suc ?i) ?ts = drop (Suc ?i) ?bca" by simp
  also have "... = aft" by simp
  finally have aft: "map (map_funs_term fg) (drop (Suc ?i) ts) = aft" by (simp add:drop_map)
  let ?bda = "take ?i ts @ Du # drop (Suc ?i) ts"
  show ?case
  proof (rule exI[of _ "More f (take ?i ts) D (drop (Suc ?i) ts)"],
      rule exI[of _ u], simp add: u f D bef aft t)
    have "ts = take ?i ts @ ts ! ?i # drop (Suc ?i) ts"
      by (rule id_take_nth_drop[OF i])
    also have "... = ?bda" by (simp add: id)
    finally show "ts = ?bda" .
  qed
qed





lemma prod_automata_from_none_root_dec:
  assumes "gta_lang Q 𝒜  {gpair s t| s t. funas_gterm s    funas_gterm t  }"
    and "q |∈| ta_der 𝒜 (term_of_gterm t)" and "fst (groot_sym t) = None"
    and "𝒬 𝒜 |⊆| ta_reachable 𝒜" and "q |∈| ta_productive Q 𝒜"
  shows " u. t = gterm_to_None_Some u  funas_gterm u  "
proof -
  have *: "gfun_at t [] = Some (groot_sym t)" by (cases t) auto
  from assms(4, 5) obtain C qf where ctxt: "ground_ctxt C" and
    fin: "qf |∈| ta_der 𝒜 CVar q" "qf |∈| Q"
    by (auto simp: ta_productive_def'[OF assms(4)])
  then obtain s v where gp: "gpair s v = (gctxt_of_ctxt C)tG" and
   funas: "funas_gterm v  "
    using assms(1, 2) gta_langI[OF fin(2), of 𝒜 "(gctxt_of_ctxt C)tG"]
    by (auto simp: ta_der_ctxt ground_gctxt_of_ctxt_apply_gterm)
  from gp have mem: "hole_pos C  gposs s  gposs v"
    by auto (metis Un_iff ctxt ghole_pos_in_apply gposs_of_gpair ground_hole_pos_to_ghole)
  from this have "hole_pos C  gposs s" using assms(3)
    using arg_cong[OF gp, of "λ t. gfun_at t (hole_pos C)"]
    using ground_hole_pos_to_ghole[OF ctxt]
    using gfun_at_after_hole_pos[OF position_less_refl, of "gctxt_of_ctxt C"]
    by (auto simp: gfun_at_gpair * split: if_splits)
       (metis fstI gfun_at_None_ngposs_iff)+
  from subst_at_gpair_nt_poss_None_Some[OF _ this, of v] this
  have "t = gterm_to_None_Some (gsubt_at v (hole_pos C))  funas_gterm (gsubt_at v (hole_pos C))  "
    using funas mem funas_gterm_gsubt_at_subseteq
    by (auto simp: gp intro!: exI[of _ "gsubt_at v (hole_pos C)"])
       (metis ctxt ground_hole_pos_to_ghole gsubt_at_gctxt_apply_ghole)
  then show ?thesis 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 Q_inf_exec_impl_Q_inf:
  assumes "gta_lang Q 𝒜  {gpair s t| s t. funas_gterm s  fset   funas_gterm t  fset }"
   and "𝒬 𝒜 |⊆| ta_reachable 𝒜" and "𝒬 𝒜 |⊆| ta_productive Q 𝒜"
   and "q  Q_inf_e 𝒜"
  shows "q |∈| Q_infty 𝒜 "
proof -
  let ?S = "{t. q |∈| ta_der 𝒜 (term_of_gterm t)  fst (groot_sym t) = None}"
  let ?P = "λ t. funas_gterm t  fset   q |∈| ta_der 𝒜 (term_of_gterm (gterm_to_None_Some t))"
  let ?F = "(λ(f, n). ((None, Some f), n)) |`| "
  from Q_inf_e_infinite_terms_res[OF assms(4, 2)] have inf: "infinite ?S" by auto
  {fix t assume "t  ?S"
    then have " u. t = gterm_to_None_Some u  funas_gterm u  fset "
      using prod_automata_from_none_root_dec[OF assms(1)] assms(2, 3)
      using fin_mono by fastforce}
  then show ?thesis using infinite_set_dec_infinite[OF inf, of gterm_to_None_Some ?P]
    by (auto simp: Q_infty_fmember) blast
qed


lemma Q_inf_impl_Q_inf_exec:
  assumes "q |∈| Q_infty 𝒜 "
    shows "q  Q_inf_e 𝒜"
proof -
  let ?t_of_g = "λ t. term_of_gterm t :: ('b option × 'b option, 'a) term"
  let ?t_og_g2 = "λ t. term_of_gterm t :: ('b, 'a) term"
  let ?inf = "(?t_og_g2 :: 'b gterm  ('b, 'a) term) ` {t |t. funas_gterm t  fset   q |∈| ta_der 𝒜 (?t_of_g (gterm_to_None_Some t))}"
  obtain n where card_st: "fcard (𝒬 𝒜) < n" by blast
  from assms(1) have "infinite {t |t. funas_gterm t  fset   q |∈| ta_der 𝒜 (?t_of_g (gterm_to_None_Some t))}"
    unfolding Q_infty_def by blast
  from infinite_inj_image_infinite[OF this, of "?t_og_g2"] have inf: "infinite ?inf" using inj_term_of_gterm by blast
  {fix s assume "s  ?inf" then have "ground s" "funas_term s  fset " by (auto simp: funas_term_of_gterm_conv subsetD)}
  from infinte_no_depth_limit[OF inf, of "fset "] this obtain u where
    funas: "funas_gterm u  fset " and card_d: "n < depth (?t_og_g2 u)" and reach: "q |∈| ta_der 𝒜 (?t_of_g (gterm_to_None_Some u))"
    by auto blast
  have "depth (?t_og_g2 u) = depth (?t_of_g (gterm_to_None_Some u))"
  proof (induct u)
    case (GFun f ts) then show ?case
      by (auto simp: comp_def intro: nth_args_depth_eqI)
  qed 
  from this pigeonhole_tree_automata[OF _ reach] card_st card_d obtain C2 C s v p where
    ctxt: "C2  " "Cs = term_of_gterm (gterm_to_None_Some u)" "C2v = s" and
    loop: "p |∈| ta_der 𝒜 v  p |∈| ta_der 𝒜 C2Var p  q |∈| ta_der 𝒜 CVar p"
    by auto
  from ctxt have gr: "ground_ctxt C2" "ground_ctxt C" by auto (metis ground_ctxt_apply ground_term_of_gterm)+ 
  from ta_der_to_ta_strict[OF _ gr(1)] loop obtain q' where
    to_strict: "(p = q'  (p, q') |∈| (eps 𝒜)|+|)  p |∈| ta_der_strict 𝒜 C2Var q'" by fastforce
  have *: " C. C2 = map_funs_ctxt lift_None_Some C  C  " using ctxt(1, 2)
    by (auto simp flip: ctxt(3)) (smt ctxt.simps(8) map_funs_term_ctxt_decomp map_term_of_gterm)
  then have q_p: "(q', p)  Q_inf 𝒜" using to_strict ta_der_Q_inf[of p 𝒜 _  q'] ctxt
    by auto
  then have cycle: "(q', q')  Q_inf 𝒜" using to_strict by (auto intro: Q_inf_ta_eps_Q_inf)
  show ?thesis
  proof (cases "C = ")
    case True then show ?thesis
      using cycle q_p loop by (auto intro: Q_inf_ta_eps_Q_inf)
  next
    case False
    obtain q'' where r: "p = q''  (p, q'') |∈| (eps 𝒜)|+|" "q |∈| ta_der_strict 𝒜 CVar q''"
      using ta_der_to_ta_strict[OF conjunct2[OF conjunct2[OF loop]] gr(2)] by auto
    then have "(q'', q)   Q_inf 𝒜" using ta_der_Q_inf[of q 𝒜 _  q''] ctxt False
      by auto (smt (z3) ctxt.simps(8) map_funs_term_ctxt_decomp map_term_of_gterm)+
    then show ?thesis using r(1) cycle q_p
      by (auto simp: Q_inf_ta_eps_Q_inf intro!: exI[of _ q'])
         (meson Q_inf.trans Q_inf_ta_eps_Q_inf)+   
  qed
qed

lemma Q_infty_fQ_inf_e_conv:
  assumes "gta_lang Q 𝒜  {gpair s t| s t. funas_gterm s  fset   funas_gterm t  fset }"
   and "𝒬 𝒜 |⊆| ta_reachable 𝒜" and "𝒬 𝒜 |⊆| ta_productive Q 𝒜"
  shows "Q_infty 𝒜  = fQ_inf_e 𝒜"
  using Q_inf_impl_Q_inf_exec Q_inf_exec_impl_Q_inf[OF assms]
  by (auto simp: fQ_inf_e.rep_eq) fastforce

definition Inf_reg_impl where
  "Inf_reg_impl R = Inf_reg R (fQ_inf_e (ta R))"

lemma Inf_reg_impl_sound:
  assumes " 𝒜  {gpair s t| s t. funas_gterm s  fset   funas_gterm t  fset }"
   and "𝒬r 𝒜 |⊆| ta_reachable (ta 𝒜)" and "𝒬r 𝒜 |⊆| ta_productive (fin 𝒜) (ta 𝒜)"
  shows " (Inf_reg_impl 𝒜) =  (Inf_reg 𝒜 (Q_infty (ta 𝒜) ))"
  using Q_infty_fQ_inf_e_conv[of "fin 𝒜" "ta 𝒜" ] assms[unfolded ℒ_def]
  by (simp add: Inf_reg_impl_def)

end