[STATEMENT]
lemma Q_infer1:
  "infer1 pq X = {(fst pq, r) | q r. (q, r) |\<in>| eps A \<and> q = snd pq} \<union>
    {(r, snd pq) |r p'. (r, p') \<in> X \<and> p' = fst pq} \<union>
    {(fst pq, r) |q' r. (q', r) \<in> (insert pq X) \<and> q' = snd pq}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infer1 pq X = {uu_. \<exists>q r. uu_ = (fst pq, r) \<and> (q, r) |\<in>| eps A \<and> q = snd pq} \<union> {uu_. \<exists>r p'. uu_ = (r, snd pq) \<and> (r, p') \<in> X \<and> p' = fst pq} \<union> {uu_. \<exists>q' r. uu_ = (fst pq, r) \<and> (q', r) \<in> insert pq X \<and> q' = snd pq}
[PROOF STEP]
unfolding Q_inf_rules_def horn_infer1_union
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. horn.infer1 {uu_. \<exists>f ps p i. uu_ = [] \<rightarrow>\<^sub>h (ps ! i, p) \<and> lift_None_Some f ps \<rightarrow> p |\<in>| rules A \<and> i < length ps} pq X \<union> horn.infer1 {[(p, q)] \<rightarrow>\<^sub>h (p, r) |p q r. (q, r) |\<in>| eps A} pq X \<union> horn.infer1 {[(p, q), (q, r)] \<rightarrow>\<^sub>h (p, r) |p q r. True} pq X = {uu_. \<exists>q r. uu_ = (fst pq, r) \<and> (q, r) |\<in>| eps A \<and> q = snd pq} \<union> {uu_. \<exists>r p'. uu_ = (r, snd pq) \<and> (r, p') \<in> X \<and> p' = fst pq} \<union> {uu_. \<exists>q' r. uu_ = (fst pq, r) \<and> (q', r) \<in> insert pq X \<and> q' = snd pq}
[PROOF STEP]
by (auto simp: horn.infer1_def simp flip: ex_simps(1)) force+