Theory Pair_Automaton

theory Pair_Automaton
  imports TR.Tree_Automata_Complement UL.Basic_Utils GTT_Compose
begin

definition pair_at_lang :: "('q, 'f) gtt ⇒ ('q × 'q) fset ⇒ 'f gterm rel" where
  "pair_at_lang 𝒢 Q = {(s, t) | s t p q. q |∈| gta_der (fst 𝒢) s ∧ p |∈| gta_der (snd 𝒢) t ∧ (q, p) |∈| Q}"

lemma pair_at_lang_restr_states:
  "pair_at_lang 𝒢 Q = pair_at_lang 𝒢 (Q |∩| (𝒬 (fst 𝒢) |×| 𝒬 (snd 𝒢)))"
  by (auto simp: pair_at_lang_def gta_der_def) (meson gterm_ta_der_states) 

lemma pair_at_langE:
  assumes "(s, t) ∈ pair_at_lang 𝒢 Q"
  obtains q p where "(q, p) |∈| Q" and "q |∈| gta_der (fst 𝒢) s" and "p |∈| gta_der (snd 𝒢) t"
  using assms by (auto simp: pair_at_lang_def)

lemma pair_at_langI:
  assumes "q |∈| gta_der (fst 𝒢) s" "p |∈| gta_der (snd 𝒢) t" "(q, p) |∈| Q"
  shows "(s, t) ∈ pair_at_lang 𝒢 Q"
  using assms by (auto simp: pair_at_lang_def)

lemma pair_at_lang_fun_states:
  assumes "finj_on f (𝒬 (fst 𝒢))" and "finj_on g (𝒬 (snd 𝒢))"
    and "Q |⊆| 𝒬 (fst 𝒢) |×| 𝒬 (snd 𝒢)"
  shows "pair_at_lang 𝒢 Q = pair_at_lang (map_prod (fmap_states_ta f) (fmap_states_ta g) 𝒢) (map_prod f g |`| Q)"
    (is "?LS = ?RS")
proof
  {fix s t assume "(s, t) ∈ ?LS"
    then have "(s, t) ∈ ?RS" using ta_der_fmap_states_ta_mono[of f "fst 𝒢" s]
      using ta_der_fmap_states_ta_mono[of g "snd 𝒢" t]
      by (force simp: gta_der_def map_prod_def image_iff  elim!: pair_at_langE split: prod.split intro!: pair_at_langI)}
  then show "?LS ⊆ ?RS" by auto
next
  {fix s t assume "(s, t) ∈ ?RS"
    then obtain p q where rs: "p |∈| ta_der (fst 𝒢) (term_of_gterm s)" "f p |∈| ta_der (fmap_states_ta f (fst 𝒢)) (term_of_gterm s)" and
      ts: "q |∈| ta_der (snd 𝒢) (term_of_gterm t)" "g q |∈| ta_der (fmap_states_ta g (snd 𝒢)) (term_of_gterm t)" and
      st: "(f p, g q) |∈| (map_prod f g |`| Q)" using assms ta_der_fmap_states_inv[of f "fst 𝒢" _ s]
      using ta_der_fmap_states_inv[of g "snd 𝒢" _ t]
      by (auto simp: gta_der_def adapt_vars_term_of_gterm elim!: pair_at_langE)
         (metis (no_types, hide_lams) fimageE fmap_prod_fimageI ta_der_fmap_states_conv)
    then have "p |∈| 𝒬 (fst 𝒢)" "q |∈| 𝒬 (snd 𝒢)" by auto
    then have "(p, q) |∈| Q" using assms st unfolding fimage_iff fBex_def
      by (auto dest!: fsubsetD simp: finj_on_eq_iff)
    then have "(s, t) ∈ ?LS" using st rs(1) ts(1) by (auto simp: gta_der_def intro!: pair_at_langI)}
  then show "?RS ⊆ ?LS" by auto
qed

lemma converse_pair_at_lang:
  "(pair_at_lang 𝒢 Q)¯ = pair_at_lang (prod.swap 𝒢) (Q|¯|)"
  by (auto simp: pair_at_lang_def)

lemma pair_at_agtt:
  "agtt_lang 𝒢 = pair_at_lang 𝒢 (fId_on (gtt_interface 𝒢))"
  by (auto simp: agtt_lang_def gtt_interface_def pair_at_lang_def gtt_states_def gta_der_def fId_on_iff)

definition Δ_eps_pair where
  "Δ_eps_pair 𝒢⇩1 Q⇩1 𝒢⇩2 Q⇩2 ≡  Q⇩1 |O| Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2) |O| Q⇩2"

lemma pair_comp_sound1:
  assumes "(s, t) ∈ pair_at_lang 𝒢⇩1 Q⇩1"
    and "(t, u) ∈ pair_at_lang 𝒢⇩2 Q⇩2"
  shows "(s, u) ∈ pair_at_lang (fst 𝒢⇩1, snd 𝒢⇩2) (Δ_eps_pair 𝒢⇩1 Q⇩1 𝒢⇩2 Q⇩2)"
proof -
  from pair_at_langE assms obtain p q  q' r where
    wit: "(p, q) |∈| Q⇩1" "p |∈| gta_der (fst 𝒢⇩1) s" "q |∈| gta_der (snd 𝒢⇩1) t"
    "(q', r) |∈| Q⇩2" "q' |∈| gta_der (fst 𝒢⇩2) t" "r |∈| gta_der (snd 𝒢⇩2) u"
      by metis
  from wit(3, 5) have "(q, q') |∈| Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2)"
    by (auto simp: Δ⇩ε_def' gta_der_def intro!: exI[of _ "term_of_gterm t"])
  then have "(p, r) |∈| Δ_eps_pair 𝒢⇩1 Q⇩1 𝒢⇩2 Q⇩2" using wit(1, 4)
    by (auto simp: Δ_eps_pair_def)
  then show ?thesis using wit(2, 6) unfolding pair_at_lang_def
    by auto
qed

lemma pair_comp_sound2:
  assumes "(s, u) ∈  pair_at_lang (fst 𝒢⇩1, snd 𝒢⇩2) (Δ_eps_pair 𝒢⇩1 Q⇩1 𝒢⇩2 Q⇩2)"
  shows "∃ t. (s, t) ∈ pair_at_lang 𝒢⇩1 Q⇩1 ∧ (t, u) ∈ pair_at_lang 𝒢⇩2 Q⇩2"
  using assms unfolding pair_at_lang_def Δ_eps_pair_def
  by (auto simp: Δ⇩ε_def' gta_der_def) (metis gterm_of_term_inv)

lemma pair_comp_sound:
  "pair_at_lang 𝒢⇩1 Q⇩1 O pair_at_lang 𝒢⇩2 Q⇩2 = pair_at_lang (fst 𝒢⇩1, snd 𝒢⇩2) (Δ_eps_pair 𝒢⇩1 Q⇩1 𝒢⇩2 Q⇩2)"
  by (auto simp: pair_comp_sound1 pair_comp_sound2 relcomp.simps)

inductive_set Δ_Atrans_set :: "('q × 'q) fset ⇒ ('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) set" for Q 𝒜 ℬ where
  base [simp]: "(p, q) |∈| Q ⟹ (p, q) ∈ Δ_Atrans_set Q 𝒜 ℬ"
| step [intro]: "(p, q) ∈ Δ_Atrans_set Q 𝒜 ℬ ⟹ (q, r) |∈| Δ⇩ε ℬ 𝒜 ⟹
     (r, v) ∈ Δ_Atrans_set Q 𝒜 ℬ ⟹ (p, v) ∈ Δ_Atrans_set Q 𝒜 ℬ"

lemma Δ_Atrans_set_states:
  "(p, q) ∈ Δ_Atrans_set Q 𝒜 ℬ ⟹ (p, q) ∈ fset ((fst |`| Q |∪| 𝒬 𝒜) |×| (snd |`| Q |∪| 𝒬 ℬ))"
  by (induct rule: Δ_Atrans_set.induct) (auto simp: fimage_iff fBex_def simp flip: fmember.rep_eq)

lemma finite_Δ_Atrans_set: "finite (Δ_Atrans_set Q 𝒜 ℬ)"
proof -
  have "Δ_Atrans_set Q 𝒜 ℬ ⊆ fset ((fst |`| Q |∪| 𝒬 𝒜) |×| (snd |`| Q |∪| 𝒬 ℬ))"
    using Δ_Atrans_set_states by auto
  from finite_subset[OF this] show ?thesis by simp
qed

context
includes fset.lifting
begin
lift_definition Δ_Atrans ::  "('q × 'q) fset ⇒ ('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) fset" is Δ_Atrans_set
  by (simp add: finite_Δ_Atrans_set)

lemmas Δ_Atrans_base [simp] = Δ_Atrans_set.base [Transfer.transferred]
lemmas Δ_Atrans_step [intro] = Δ_Atrans_set.step [Transfer.transferred]
lemmas Δ_Atrans_cases = Δ_Atrans_set.cases[Transfer.transferred]
lemmas Δ_Atrans_induct [consumes 1, case_names base step] = Δ_Atrans_set.induct[Transfer.transferred]
end

"Δ_Atrans_gtt 𝒢 Q ≡ Δ_Atrans Q (fst 𝒢) (snd 𝒢)"">abbreviation "Δ_Atrans_gtt 𝒢 Q ≡ Δ_Atrans Q (fst 𝒢) (snd 𝒢)"

lemma pair_trancl_sound1:
  assumes "(s, t) ∈ (pair_at_lang 𝒢 Q)⇧+"
  shows "∃ q p. p |∈| gta_der (fst 𝒢) s ∧ q |∈| gta_der (snd 𝒢) t ∧ (p, q) |∈| Δ_Atrans_gtt 𝒢 Q"
  using assms
proof (induct)
  case (step t v)
  obtain p q r r' where reach_t: "r |∈| gta_der (fst 𝒢) t" "q |∈| gta_der (snd 𝒢) t" and
    reach: "p |∈| gta_der (fst 𝒢) s" "r' |∈| gta_der (snd 𝒢) v" and
    st: "(p, q) |∈| Δ_Atrans_gtt 𝒢 Q"  "(r, r') |∈| Q" using step(2, 3)
    by (auto simp: pair_at_lang_def)
  from reach_t have "(q, r) |∈| Δ⇩ε (snd 𝒢) (fst 𝒢)"
    by (auto simp: Δ⇩ε_def' gta_der_def intro: ground_term_of_gterm)
  then have "(p, r') |∈| Δ_Atrans_gtt 𝒢 Q" using st by auto
  then show ?case using reach reach_t
    by (auto simp: pair_at_lang_def gta_der_def Δ⇩ε_def' intro: ground_term_of_gterm)
qed (auto simp: pair_at_lang_def intro: Δ_Atrans_base)

lemma pair_trancl_sound2:
  assumes "(p, q) |∈| Δ_Atrans_gtt 𝒢 Q"
    and "p |∈| gta_der (fst 𝒢) s" "q |∈| gta_der (snd 𝒢) t"
  shows "(s, t) ∈ (pair_at_lang 𝒢 Q)⇧+" using assms
proof (induct arbitrary: s t rule:Δ_Atrans_induct)
  case (step p q r v)
  from step(2)[OF step(6)] step(5)[OF _ step(7)] step(3)
  show ?case by (auto simp: gta_der_def Δ⇩ε_def' intro!: ground_term_of_gterm)
      (metis gterm_of_term_inv trancl_trans)
qed (auto simp: pair_at_lang_def)

lemma pair_trancl_sound:
  "(pair_at_lang 𝒢 Q)⇧+ = pair_at_lang 𝒢 (Δ_Atrans_gtt 𝒢 Q)"
  by (auto simp: pair_trancl_sound2 dest: pair_trancl_sound1 elim: pair_at_langE intro: pair_at_langI)

"fst_pair_cl 𝒜 Q ≡ TA (rules 𝒜) (eps 𝒜 |∪| (fId_on (𝒬 𝒜) |O| Q))"">abbreviation "fst_pair_cl 𝒜 Q ≡ TA (rules 𝒜) (eps 𝒜 |∪| (fId_on (𝒬 𝒜) |O| Q))"
definition pair_at_to_agtt :: "('q, 'f) gtt ⇒ ('q × 'q) fset ⇒ ('q, 'f) gtt" where
  "pair_at_to_agtt 𝒢 Q = (fst_pair_cl (fst 𝒢) Q , TA (rules (snd 𝒢)) (eps (snd 𝒢)))"

lemma fst_pair_cl_eps:
  assumes "(p, q) |∈| (eps (fst_pair_cl 𝒜 Q))|⇧+|"
    and "𝒬 𝒜 |∩| snd |`| Q = {||}"
  shows "(p, q) |∈| (eps 𝒜)|⇧+| ∨ (∃ r. (p = r ∨ (p, r) |∈| (eps 𝒜)|⇧+|) ∧ (r, q) |∈| Q)" using assms
proof (induct rule: ftrancl_induct)
  case (Step p q r)
  then have y: "q |∈| 𝒬 𝒜" by (auto simp add: eps_trancl_statesD eps_statesD)
  have [simp]: "(p, q) |∈| Q ⟹ q |∈| snd |`| Q" for p q by (auto simp: fimage_iff) force 
  then show ?case using Step y
    by auto (simp add: ftrancl_into_trancl)
qed auto

lemma fst_pair_cl_res_aux:
  assumes "𝒬 𝒜 |∩| snd |`| Q = {||}"
    and "q |∈| ta_der (fst_pair_cl 𝒜 Q) (term_of_gterm t)"
  shows "∃ p. p |∈| ta_der 𝒜 (term_of_gterm t) ∧ (q |∉| 𝒬 𝒜 ⟶ (p, q) |∈| Q) ∧ (q |∈| 𝒬 𝒜 ⟶ p = q)" using assms
proof (induct t arbitrary: q)
  case (GFun f ts)
  then obtain qs q' where rule: "TA_rule f qs q' |∈| rules 𝒜" "length qs = length ts" and
    eps: "q' = q ∨ (q', q) |∈| (eps (fst_pair_cl 𝒜 Q))|⇧+|" and
    reach: "∀ i < length ts. qs ! i |∈| ta_der (fst_pair_cl 𝒜 Q) (term_of_gterm (ts ! i))"
    by auto
  {fix i assume ass: "i < length ts" then have st: "qs ! i |∈| 𝒬 𝒜" using rule
      by (auto simp: rule_statesD)
    then have "qs ! i |∉| snd |`| Q" using GFun(2) by auto
    then have "qs ! i |∈| ta_der 𝒜 (term_of_gterm (ts ! i))" using reach st ass
      using fst_pair_cl_eps[OF _ GFun(2)] GFun(1)[OF nth_mem[OF ass] GFun(2), of "qs ! i"]
      by blast} note IH = this
  show ?case
  proof (cases "q' = q")
    case True
    then show ?thesis using rule reach IH
      by (auto dest: rule_statesD intro!: exI[of _ q'] exI[of _ qs])
  next
    case False note nt_eq = this
    then have eps: "(q', q) |∈| (eps (fst_pair_cl 𝒜 Q))|⇧+|" using eps by simp
    from fst_pair_cl_eps[OF this assms(1)] show ?thesis
      using False rule IH
    proof (cases "q |∉| 𝒬 𝒜")
      case True
      from fst_pair_cl_eps[OF eps assms(1)] obtain r where
         "q' = r ∨ (q', r) |∈| (eps 𝒜)|⇧+|" "(r, q) |∈| Q" using True
        by (auto simp: eps_trancl_statesD)
      then show ?thesis using nt_eq rule IH True
        by (auto simp: fimage_iff eps_trancl_statesD)
    next
      case False
      from fst_pair_cl_eps[OF eps assms(1)] False assms(1)
      have "(q', q) |∈| (eps 𝒜)|⇧+|"
        by (auto simp: fimage_iff) (metis fempty_iff fimage_eqI finterI snd_conv)+
      then show ?thesis using IH rule
        by (intro exI[of _ q]) (auto simp: eps_trancl_statesD)
    qed
  qed
qed

lemma restr_distjoing:
  assumes "Q |⊆| 𝒬 𝒜 |×| 𝒬 𝔅"
    and "𝒬 𝒜 |∩| 𝒬 𝔅 = {||}"
  shows "𝒬 𝒜 |∩| snd |`| Q = {||}"
  using assms by auto

lemma pair_at_agtt_conv:
  assumes "Q |⊆| 𝒬 (fst 𝒢) |×| 𝒬 (snd 𝒢)" and "𝒬 (fst 𝒢) |∩| 𝒬 (snd 𝒢) = {||}"
  shows "pair_at_lang 𝒢 Q = agtt_lang (pair_at_to_agtt 𝒢 Q)" (is "?LS = ?RS")
proof
  let ?TA = "fst_pair_cl (fst 𝒢) Q"
  {fix s t assume ls: "(s, t) ∈ ?LS"
    then obtain q p where w: "(q, p) |∈| Q" "q |∈| gta_der (fst 𝒢) s" "p |∈| gta_der (snd 𝒢) t"
      by (auto elim: pair_at_langE)
    from w(2) have "q |∈| gta_der ?TA s" "q |∈| 𝒬 (fst 𝒢)"
      using ta_der_mono'[of "fst 𝒢" ?TA "term_of_gterm s"]
      by (auto simp add: fin_mono ta_subset_def gta_der_def in_mono)
    then have "(s, t) ∈ ?RS" using w(1, 3)
      by (auto simp: pair_at_to_agtt_def agtt_lang_def gta_der_def ta_der_eps intro!: exI[of _ p])
         (metis fId_onI frelcompI funionI2 ta.sel(2) ta_der_eps)}
  then show "?LS ⊆ ?RS" by auto
next
  {fix s t assume ls: "(s, t) ∈ ?RS"
    then obtain q where w: "q |∈| ta_der (fst_pair_cl (fst 𝒢) Q) (term_of_gterm s)"
      "q |∈| ta_der (snd 𝒢) (term_of_gterm t)"
      by (auto simp: agtt_lang_def pair_at_to_agtt_def gta_der_def)
    from w(2) have "q |∈| 𝒬 (snd 𝒢)" "q |∉| 𝒬 (fst 𝒢)" using assms(2)
      by auto
    from fst_pair_cl_res_aux[OF restr_distjoing[OF assms] w(1)] this w(2)
    have "(s, t) ∈ ?LS" by (auto simp: agtt_lang_def pair_at_to_agtt_def gta_der_def intro: pair_at_langI)}
  then show "?RS ⊆ ?LS" by auto
qed

definition pair_at_to_agtt' where
  "pair_at_to_agtt' 𝒢 Q = (let 𝒜 = fmap_states_ta Inl (fst 𝒢) in
    let ℬ = fmap_states_ta Inr (snd 𝒢) in
    let Q' = Q |∩| (𝒬 (fst 𝒢) |×| 𝒬 (snd 𝒢)) in
    pair_at_to_agtt (𝒜, ℬ) (map_prod Inl Inr |`| Q'))"

lemma pair_at_agtt_cost:
  "pair_at_lang 𝒢 Q = agtt_lang (pair_at_to_agtt' 𝒢 Q)"
proof -
  let ?G = "(fmap_states_ta CInl (fst 𝒢), fmap_states_ta CInr (snd 𝒢))"
  let ?Q = "(Q |∩| (𝒬 (fst 𝒢) |×| 𝒬 (snd 𝒢)))"
  let ?Q' = "map_prod CInl CInr |`| ?Q"
  have *: "pair_at_lang 𝒢 Q = pair_at_lang 𝒢 ?Q"
    using pair_at_lang_restr_states by blast
  have "pair_at_lang 𝒢 ?Q = pair_at_lang (map_prod (fmap_states_ta CInl) (fmap_states_ta CInr) 𝒢) (map_prod CInl CInr |`| ?Q)"
    by (intro pair_at_lang_fun_states[where ?𝒢 = 𝒢 and ?Q = ?Q and ?f = CInl and ?g = CInr])
       (auto simp: finj_CInl_CInr)
  then have **:"pair_at_lang 𝒢 ?Q = pair_at_lang ?G ?Q'" by (simp add: map_prod_simp')
  have "pair_at_lang ?G ?Q' = agtt_lang (pair_at_to_agtt ?G ?Q')"
    by (intro pair_at_agtt_conv[where ?𝒢 = ?G]) auto
  then show ?thesis unfolding * ** pair_at_to_agtt'_def Let_def
    by simp
qed

lemma Δ_Atrans_states_stable:
  assumes "Q |⊆| 𝒬 (fst 𝒢) |×| 𝒬 (snd 𝒢)"
  shows "Δ_Atrans_gtt 𝒢 Q |⊆| 𝒬 (fst 𝒢) |×| 𝒬 (snd 𝒢)"
proof
  fix s assume ass: "s |∈| Δ_Atrans_gtt 𝒢 Q"
  then obtain t u where s: "s = (t, u)" by (cases s) blast
  show "s |∈| 𝒬 (fst 𝒢) |×| 𝒬 (snd 𝒢)" using ass assms unfolding s
    by (induct rule: Δ_Atrans_induct) auto
qed

lemma Δ_Atrans_map_prod:
  assumes "finj_on f (𝒬 (fst 𝒢))" and "finj_on g (𝒬 (snd 𝒢))"
    and "Q |⊆| 𝒬 (fst 𝒢) |×| 𝒬 (snd 𝒢)"
  shows "map_prod f g |`| (Δ_Atrans_gtt 𝒢 Q) = Δ_Atrans_gtt (map_prod (fmap_states_ta f) (fmap_states_ta g) 𝒢) (map_prod f g |`| Q)"
    (is "?LS = ?RS")
proof -
  {fix p q assume "(p, q) |∈| Δ_Atrans_gtt 𝒢 Q"
    then have "(f p, g q) |∈| ?RS" using assms
    proof (induct rule: Δ_Atrans_induct)
      case (step p q r v)
      from step(3, 6, 7) have "(g q, f r) |∈| Δ⇩ε (fmap_states_ta g (snd 𝒢)) (fmap_states_ta f (fst 𝒢))"
        by (auto simp: Δ⇩ε_def' intro!: ground_term_of_gterm)
           (metis ground_term_of_gterm ground_term_to_gtermD ta_der_to_fmap_states_der)
      then show ?case using step by auto
    qed (auto simp add: fmap_prod_fimageI)}
  moreover
  {fix p q assume "(p, q) |∈| ?RS"
    then have "(p, q) |∈| ?LS" using assms
    proof (induct rule: Δ_Atrans_induct)
      case (step p q r v)
      let ?f = "the_finv_into (𝒬 (fst 𝒢)) f" let ?g = "the_finv_into (𝒬 (snd 𝒢)) g"
      have sub: "Δ⇩ε (snd 𝒢) (fst 𝒢) |⊆| 𝒬 (snd 𝒢) |×| 𝒬 (fst 𝒢)"
        using Δ⇩ε_statesD(1, 2) by fastforce
      have s_e: "(?f p, ?g q) |∈| Δ_Atrans_gtt 𝒢 Q" "(?f r, ?g v) |∈| Δ_Atrans_gtt 𝒢 Q"
        using step assms(1, 2) fsubsetD[OF Δ_Atrans_states_stable[OF assms(3)]]
        using finj_on_eq_iff[OF assms(1)] finj_on_eq_iff
        using the_finv_into_f_f[OF assms(1)] the_finv_into_f_f[OF assms(2)]
        by auto
      from step(3) have "(?g q, ?f r) |∈| Δ⇩ε (snd 𝒢) (fst 𝒢)"
        using step(6-) sub
        using ta_der_fmap_states_conv[OF assms(1)] ta_der_fmap_states_conv[OF assms(2)]
        using the_finv_into_f_f[OF assms(1)] the_finv_into_f_f[OF assms(2)]
        by (auto simp: Δ⇩ε_fmember fimage_iff fBex_def)
           (metis ground_term_of_gterm ground_term_to_gtermD ta_der_fmap_states_inv)
      then have "(q, r) |∈| map_prod g f |`| Δ⇩ε (snd 𝒢) (fst 𝒢)" using step
        using the_finv_into_f_f[OF assms(1)] the_finv_into_f_f[OF assms(2)] sub
        by auto (smt Δ⇩ε_statesD(1, 2) f_the_finv_into_f fmap_prod_fimageI fmap_states)
      then show ?case using s_e assms(1, 2) s_e
        using fsubsetD[OF sub]
        using fsubsetD[OF Δ_Atrans_states_stable[OF assms(3)]]
        using Δ_Atrans_step[of "?f p" "?g q" Q "fst 𝒢" "snd 𝒢" "?f r" "?g v"]
        using the_finv_into_f_f[OF assms(1)] the_finv_into_f_f[OF assms(2)]
        by  (auto simp: fimage_iff fBex_def)
            (smt Pair_inject prod_fun_fimageE step.hyps(2) step.hyps(5) step.prems(3))
    qed auto}
  ultimately show ?thesis by auto
qed

― ‹Section: Pair Automaton is closed under Determinization›

"Q_pow Q 𝒮_1 𝒮_2 =">definition "Q_pow Q 𝒮⇩1 𝒮⇩2 =
  {|(X, Y) | X Y p q. X |∈| fPow 𝒮⇩1 ∧ Y |∈| fPow 𝒮⇩2 ∧ p |∈| X ∧ q |∈| Y ∧ (p, q) |∈| Q|}"

lemma Q_pow_fmember:
  "(X, Y) |∈| Q_pow Q 𝒮⇩1 𝒮⇩2 ⟷ (∃ p q. X |∈| fPow 𝒮⇩1 ∧ Y |∈| fPow 𝒮⇩2 ∧ p |∈| X ∧ q |∈| Y ∧ (p, q) |∈| Q)"
proof -
  have "{(X, Y) | X Y p q. X |∈| fPow 𝒮⇩1 ∧ Y |∈| fPow 𝒮⇩2 ∧ p |∈| X ∧ q |∈| Y ∧ (p, q) |∈| Q} ⊆ fset (fPow 𝒮⇩1 |×| fPow 𝒮⇩2)"
    by (auto simp flip: fmember.rep_eq)
  from finite_subset[OF this] show ?thesis unfolding Q_pow_def
    by auto
qed

lemma pair_automaton_det_lang_sound_complete:
  "pair_at_lang 𝒢 Q = pair_at_lang (map_both ps_ta 𝒢) (Q_pow Q (𝒬 (fst 𝒢)) (𝒬 (snd 𝒢)))" (is "?LS = ?RS")
proof -
  {fix s t assume "(s, t) ∈ ?LS"
    then obtain  p q where
      res : "p |∈| ta_der (fst 𝒢) (term_of_gterm s)"
      "q |∈| ta_der (snd 𝒢) (term_of_gterm t)" "(p, q) |∈| Q"
      by (auto simp: pair_at_lang_def gta_der_def)
    from ps_rules_complete[OF this(1)] ps_rules_complete[OF this(2)] this(3)
    have "(s, t) ∈ ?RS" using fPow_iff ps_ta_states
      by (auto simp:  pair_at_lang_def gta_der_def Q_pow_fmember)
         force}
  moreover
  {fix s t assume "(s, t) ∈ ?RS" then have "(s, t) ∈ ?LS"
      using ps_rules_sound
      by (auto simp: pair_at_lang_def gta_der_def ps_ta_def Let_def Q_pow_def) blast}
  ultimately show ?thesis by auto
qed

lemma pair_automaton_complement_sound_complete:
  assumes "completely_defined_on 𝒜 ℱ" and "completely_defined_on ℬ ℱ"
    and "ta_det 𝒜" and "ta_det ℬ"
  shows "pair_at_lang (𝒜, ℬ) (𝒬 𝒜 |×| 𝒬 ℬ |-| Q) = gterms (fset ℱ) × gterms (fset ℱ) - pair_at_lang (𝒜, ℬ) Q"
  using assms unfolding completely_defined_on_def pair_at_lang_def
  apply (auto simp: gta_der_def)
  apply (metis ta_detE)
  apply fastforce
  done
(*
lemma pair_automaton_lang_on:
  fixes 𝒢 defines "ℱ⇩1 ≡ ta_sig (fst 𝒢)" and "ℱ⇩2 ≡ ta_sig (snd 𝒢)"
  shows "pair_at_lang 𝒢 Q ⊆ gterms (fset ℱ⇩1) × gterms (fset ℱ⇩2)"
  using assms funas_term_of_gterm_conv
  by (auto simp: pair_at_lang_def gta_der_def) fastforce+
*)
end