[STATEMENT]
lemma gcsort_count_inv:
  assumes
    A: "index_less index key" and
    B: "add_inv n t" and
    C: "n \<le> p"
  shows "\<lbrakk>t' \<in> gcsort_set index key p t; count_inv f t\<rbrakk> \<Longrightarrow>
    count_inv f t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' \<in> gcsort_set index key p t; count_inv f t\<rbrakk> \<Longrightarrow> count_inv f t'
[PROOF STEP]
by (erule gcsort_set.induct, simp, drule gcsort_add_inv [OF A _ B C],
 rule round_count_inv [OF A], simp_all del: bn_inv.simps, erule conjE,
 frule sym, erule subst, rule bn_inv_intro, insert C, simp)


[STATEMENT]
theorem gcsort_count:
  assumes
    A: "index_less index key" and
    B: "length xs \<le> p"
  shows "count (mset (gcsort index key p xs)) x = count (mset xs) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (mset (gcsort index key p xs)) x = count (mset xs) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. count (mset (gcsort index key p xs)) x = count (mset xs) x
[PROOF STEP]
let ?t = "(0, [length xs], xs)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. count (mset (gcsort index key p xs)) x = count (mset xs) x
[PROOF STEP]
have "count_inv (count (mset xs)) (gcsort_aux index key p ?t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_inv (count (mset xs)) (gcsort_aux index key p (0, [length xs], xs))
[PROOF STEP]
by (rule gcsort_count_inv [OF A _ B], rule gcsort_add_input,
     rule gcsort_aux_set, rule gcsort_count_input)
[PROOF STATE]
proof (state)
this:
count_inv (count (mset xs)) (gcsort_aux index key p (0, [length xs], xs))

goal (1 subgoal):
 1. count (mset (gcsort index key p xs)) x = count (mset xs) x
[PROOF STEP]
hence "count (mset (gcsort_out (gcsort_aux index key p ?t))) x =
    (count (mset xs)) x"
[PROOF STATE]
proof (prove)
using this:
count_inv (count (mset xs)) (gcsort_aux index key p (0, [length xs], xs))

goal (1 subgoal):
 1. count (mset (gcsort_out (gcsort_aux index key p (0, [length xs], xs)))) x = count (mset xs) x
[PROOF STEP]
by (rule gcsort_count_intro)
[PROOF STATE]
proof (state)
this:
count (mset (gcsort_out (gcsort_aux index key p (0, [length xs], xs)))) x = count (mset xs) x

goal (1 subgoal):
 1. count (mset (gcsort index key p xs)) x = count (mset xs) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
count (mset (gcsort_out (gcsort_aux index key p (0, [length xs], xs)))) x = count (mset xs) x

goal (1 subgoal):
 1. count (mset (gcsort index key p xs)) x = count (mset xs) x
[PROOF STEP]
have "?t = gcsort_in xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0, [length xs], xs) = gcsort_in xs
[PROOF STEP]
by (simp add: gcsort_in_def)
[PROOF STATE]
proof (state)
this:
(0, [length xs], xs) = gcsort_in xs

goal (1 subgoal):
 1. count (mset (gcsort index key p xs)) x = count (mset xs) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
count (mset (gcsort_out (gcsort_aux index key p (0, [length xs], xs)))) x = count (mset xs) x
(0, [length xs], xs) = gcsort_in xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
count (mset (gcsort_out (gcsort_aux index key p (0, [length xs], xs)))) x = count (mset xs) x
(0, [length xs], xs) = gcsort_in xs

goal (1 subgoal):
 1. count (mset (gcsort index key p xs)) x = count (mset xs) x
[PROOF STEP]
by (simp add: gcsort_def)
[PROOF STATE]
proof (state)
this:
count (mset (gcsort index key p xs)) x = count (mset xs) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma remove1_mset_subset_eq: "remove1_mset a A \<subseteq># B \<longleftrightarrow> A \<subseteq># add_mset a B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (remove1_mset a A \<subseteq># B) = (A \<subseteq># add_mset a B)
[PROOF STEP]
by (metis add_mset_add_single subset_eq_diff_conv)


[STATEMENT]
lemma Bex_cong: "(\<And>b. b \<in> B \<Longrightarrow> P b = Q b) \<Longrightarrow> Bex B P = Bex B Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>b. b \<in> B \<Longrightarrow> P b = Q b) \<Longrightarrow> Bex B P = Bex B Q
[PROOF STEP]
by auto


[STATEMENT]
lemma is_reducible_lit_code[code]: "RP.is_reducible_lit Ds C L =
  (\<exists>D \<in> set Ds. (\<exists>L' \<in> set D.
     if is_pos L' = is_neg L then
       (case match_term_list [(atm_of L', atm_of L)] Map.empty of
         None \<Rightarrow> False
       | Some \<sigma> \<Rightarrow> subsumes_list (remove1 L' D) C \<sigma>)
     else False))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_reducible_lit Ds C L = (\<exists>D\<in>set Ds. \<exists>L'\<in>set D. if is_pos L' = is_neg L then case match_term_list [(atm_of L', atm_of L)] Map.empty of None \<Rightarrow> False | Some \<sigma> \<Rightarrow> subsumes_list (remove1 L' D) C \<sigma> else False)
[PROOF STEP]
unfolding RP.is_reducible_lit_def subsumes_list_alt subsumes_modulo_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>D\<in>set Ds. \<exists>L'\<in>set D. \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C) = (\<exists>D\<in>set Ds. \<exists>L'\<in>set D. if is_pos L' = is_neg L then case match_term_list [(atm_of L', atm_of L)] Map.empty of None \<Rightarrow> False | Some \<sigma> \<Rightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom \<sigma> \<and> extends_subst \<sigma> \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C else False)
[PROOF STEP]
apply (rule Bex_cong)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b ba. \<lbrakk>b \<in> set Ds; ba \<in> set b\<rbrakk> \<Longrightarrow> (\<exists>\<sigma>. - L = subst_lit ba \<sigma> \<and> subst_cls (mset (remove1 ba b)) \<sigma> \<subseteq># mset C) = (if is_pos ba = is_neg L then case match_term_list [(atm_of ba, atm_of L)] Map.empty of None \<Rightarrow> False | Some \<sigma> \<Rightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 ba b)) \<union> dom \<sigma> \<and> extends_subst \<sigma> \<tau> \<and> subst_cls (mset (remove1 ba b)) (subst_of_map Var \<tau>) \<subseteq># mset C else False)
[PROOF STEP]
subgoal for D L'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D\<rbrakk> \<Longrightarrow> (\<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C) = (if is_pos L' = is_neg L then case match_term_list [(atm_of L', atm_of L)] Map.empty of None \<Rightarrow> False | Some \<sigma> \<Rightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom \<sigma> \<and> extends_subst \<sigma> \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C else False)
[PROOF STEP]
apply (split if_splits option.splits)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D\<rbrakk> \<Longrightarrow> (match_term_list [(atm_of L', atm_of L)] Map.empty = None \<longrightarrow> (is_pos L' = is_neg L \<longrightarrow> (\<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C) = False) \<and> (is_pos L' \<noteq> is_neg L \<longrightarrow> (\<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C) = False)) \<and> (\<forall>x2. match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2 \<longrightarrow> (is_pos L' = is_neg L \<longrightarrow> (\<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C) = (\<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2 \<and> extends_subst x2 \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C)) \<and> (is_pos L' \<noteq> is_neg L \<longrightarrow> (\<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C) = False))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>\<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_pos L'; is_neg L; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 2. \<And>\<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_neg L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 3. \<And>\<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_pos L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 4. \<And>\<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 5. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_neg L; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2 \<and> extends_subst x2 \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
 6. \<And>x2 \<tau>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_neg L; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2; extends_subst x2 \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
 7. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2 \<and> extends_subst x2 \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
 8. \<And>x2 \<tau>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2; extends_subst x2 \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
 9. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 10. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for \<sigma>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_pos L'; is_neg L; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using term_subst_eq[of _ "subst_of_map Var (\<lambda>x. if x \<in> vars_lit L' then Some (\<sigma> x) else None)" \<sigma>]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> vars_term ?t \<Longrightarrow> subst_of_map Var (\<lambda>x. if x \<in> vars_lit L' then Some (\<sigma> x) else None) x = \<sigma> x) \<Longrightarrow> subst_atm_abbrev ?t (subst_of_map Var (\<lambda>x. if x \<in> vars_lit L' then Some (\<sigma> x) else None)) = subst_atm_abbrev ?t \<sigma>

goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_pos L'; is_neg L; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (cases L; cases L';
        auto simp add: subst_lit_def subst_of_map_def
          dest!:  match_term_list_complete[of _ _ "\<lambda>x. if x \<in> vars_lit L' then Some (\<sigma> x) else None"])
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>\<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_neg L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 2. \<And>\<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_pos L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 3. \<And>\<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 4. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_neg L; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2 \<and> extends_subst x2 \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
 5. \<And>x2 \<tau>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_neg L; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2; extends_subst x2 \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
 6. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2 \<and> extends_subst x2 \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
 7. \<And>x2 \<tau>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2; extends_subst x2 \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
 8. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 9. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for \<sigma>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_neg L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using term_subst_eq[of _ "subst_of_map Var (\<lambda>x. if x \<in> vars_lit L' then Some (\<sigma> x) else None)" \<sigma>]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> vars_term ?t \<Longrightarrow> subst_of_map Var (\<lambda>x. if x \<in> vars_lit L' then Some (\<sigma> x) else None) x = \<sigma> x) \<Longrightarrow> subst_atm_abbrev ?t (subst_of_map Var (\<lambda>x. if x \<in> vars_lit L' then Some (\<sigma> x) else None)) = subst_atm_abbrev ?t \<sigma>

goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_neg L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (cases L; cases L';
        auto simp add: subst_lit_def subst_of_map_def
          dest!:  match_term_list_complete[of _ _ "\<lambda>x. if x \<in> vars_lit L' then Some (\<sigma> x) else None"])
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>\<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_pos L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 2. \<And>\<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 3. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_neg L; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2 \<and> extends_subst x2 \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
 4. \<And>x2 \<tau>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_neg L; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2; extends_subst x2 \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
 5. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2 \<and> extends_subst x2 \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
 6. \<And>x2 \<tau>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2; extends_subst x2 \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
 7. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 8. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for \<sigma>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_pos L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (cases L; cases L'; simp add: subst_lit_def)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>\<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 2. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_neg L; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2 \<and> extends_subst x2 \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
 3. \<And>x2 \<tau>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_neg L; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2; extends_subst x2 \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
 4. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2 \<and> extends_subst x2 \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
 5. \<And>x2 \<tau>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2; extends_subst x2 \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
 6. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 7. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for \<sigma>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = None; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (cases L; cases L'; simp add: subst_lit_def)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_neg L; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2 \<and> extends_subst x2 \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
 2. \<And>x2 \<tau>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_neg L; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2; extends_subst x2 \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
 3. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2 \<and> extends_subst x2 \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
 4. \<And>x2 \<tau>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2; extends_subst x2 \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
 5. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 6. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for \<sigma> \<tau>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some \<sigma>; is_pos L'; is_neg L; - L = subst_lit L' \<tau>; subst_cls (mset (remove1 L' D)) \<tau> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom \<sigma> \<and> extends_subst \<sigma> \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
[PROOF STEP]
using same_on_vars_clause[of "mset (remove1 L' D)" "subst_of_map Var
        (\<lambda>x. if x \<in> vars_clause (remove1_mset L' (mset D)) \<union> dom \<sigma> then Some (\<tau> x) else None)" \<tau>]
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_clause (mset (remove1 L' D)). subst_of_map Var (\<lambda>x. if x \<in> vars_clause (remove1_mset L' (mset D)) \<union> dom \<sigma> then Some (\<tau> x) else None) v = \<tau> v \<Longrightarrow> subst_cls (mset (remove1 L' D)) (subst_of_map Var (\<lambda>x. if x \<in> vars_clause (remove1_mset L' (mset D)) \<union> dom \<sigma> then Some (\<tau> x) else None)) = subst_cls (mset (remove1 L' D)) \<tau>

goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some \<sigma>; is_pos L'; is_neg L; - L = subst_lit L' \<tau>; subst_cls (mset (remove1 L' D)) \<tau> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom \<sigma> \<and> extends_subst \<sigma> \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
[PROOF STEP]
apply (cases L; cases L'; auto simp add: subst_lit_def dom_def subst_of_map_def
        dest!: match_term_list_sound split: option.splits if_splits
        intro!: exI[of _ "\<lambda>x. if x \<in> vars_clause (remove1_mset L' (mset D)) \<union> dom \<sigma> then Some (\<tau> x) else None"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>D \<in> set Ds; Pos x1 \<in> set D; subst_cls (remove1_mset (Pos x1) (mset D)) \<tau> \<subseteq># mset C; subst_cls (remove1_mset (Pos x1) (mset D)) (subst_of_map Var (\<lambda>x. if x \<in> vars_clause (remove1_mset (Pos x1) (mset D)) \<or> (\<exists>y. \<sigma> x = Some y) then Some (\<tau> x) else None)) = subst_cls (remove1_mset (Pos x1) (mset D)) \<tau>; L = Neg (subst_atm_abbrev x1 \<tau>); L' = Pos x1; {a. \<exists>y. \<sigma> a = Some y} = vars_term x1; subst_atm_abbrev x1 (subst_of_map Var \<sigma>) = subst_atm_abbrev x1 \<tau>\<rbrakk> \<Longrightarrow> extends_subst \<sigma> (\<lambda>\<tau>'. if \<tau>' \<in> vars_clause (remove1_mset (Pos x1) (mset D)) \<or> \<tau>' \<in> vars_term x1 then Some (\<tau> \<tau>') else None)
[PROOF STEP]
by (auto 0 4 simp: extends_subst_def subst_of_map_def split: option.splits dest!: term_subst_eq_rev)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x2 \<tau>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_neg L; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2; extends_subst x2 \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
 2. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2 \<and> extends_subst x2 \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
 3. \<And>x2 \<tau>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2; extends_subst x2 \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
 4. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 5. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for \<sigma> \<tau>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some \<sigma>; is_pos L'; is_neg L; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom \<sigma>; extends_subst \<sigma> \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
[PROOF STEP]
by (cases L; cases L'; auto simp add: subst_lit_def subst_of_map_def extends_subst_def
        dest!: match_term_list_sound intro!: exI[of _ "subst_of_map Var \<tau>"] term_subst_eq)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2 \<and> extends_subst x2 \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
 2. \<And>x2 \<tau>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2; extends_subst x2 \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
 3. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 4. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for \<sigma> \<tau>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some \<sigma>; is_neg L'; is_pos L; \<not> False; - L = subst_lit L' \<tau>; subst_cls (mset (remove1 L' D)) \<tau> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom \<sigma> \<and> extends_subst \<sigma> \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
[PROOF STEP]
using same_on_vars_clause[of "mset (remove1 L' D)" "subst_of_map Var
        (\<lambda>x. if x \<in> vars_clause (remove1_mset L' (mset D)) \<union> dom \<sigma> then Some (\<tau> x) else None)" \<tau>]
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vars_clause (mset (remove1 L' D)). subst_of_map Var (\<lambda>x. if x \<in> vars_clause (remove1_mset L' (mset D)) \<union> dom \<sigma> then Some (\<tau> x) else None) v = \<tau> v \<Longrightarrow> subst_cls (mset (remove1 L' D)) (subst_of_map Var (\<lambda>x. if x \<in> vars_clause (remove1_mset L' (mset D)) \<union> dom \<sigma> then Some (\<tau> x) else None)) = subst_cls (mset (remove1 L' D)) \<tau>

goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some \<sigma>; is_neg L'; is_pos L; \<not> False; - L = subst_lit L' \<tau>; subst_cls (mset (remove1 L' D)) \<tau> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<tau>. dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom \<sigma> \<and> extends_subst \<sigma> \<tau> \<and> subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C
[PROOF STEP]
apply (cases L; cases L'; auto simp add: subst_lit_def dom_def subst_of_map_def
        dest!: match_term_list_sound split: option.splits if_splits
        intro!: exI[of _ "\<lambda>x. if x \<in> vars_clause (remove1_mset L' (mset D)) \<union> dom \<sigma> then Some (\<tau> x) else None"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>D \<in> set Ds; Neg x2 \<in> set D; subst_cls (remove1_mset (Neg x2) (mset D)) \<tau> \<subseteq># mset C; subst_cls (remove1_mset (Neg x2) (mset D)) (subst_of_map Var (\<lambda>x. if x \<in> vars_clause (remove1_mset (Neg x2) (mset D)) \<or> (\<exists>y. \<sigma> x = Some y) then Some (\<tau> x) else None)) = subst_cls (remove1_mset (Neg x2) (mset D)) \<tau>; L = Pos (subst_atm_abbrev x2 \<tau>); L' = Neg x2; {a. \<exists>y. \<sigma> a = Some y} = vars_term x2; subst_atm_abbrev x2 (subst_of_map Var \<sigma>) = subst_atm_abbrev x2 \<tau>\<rbrakk> \<Longrightarrow> extends_subst \<sigma> (\<lambda>\<tau>'. if \<tau>' \<in> vars_clause (remove1_mset (Neg x2) (mset D)) \<or> \<tau>' \<in> vars_term x2 then Some (\<tau> \<tau>') else None)
[PROOF STEP]
by (auto 0 4 simp: extends_subst_def subst_of_map_def split: option.splits dest!: term_subst_eq_rev)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x2 \<tau>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L'; is_pos L; \<not> False; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom x2; extends_subst x2 \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
 2. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 3. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for \<sigma> \<tau>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some \<sigma>; is_neg L'; is_pos L; \<not> False; dom \<tau> = vars_clause (mset (remove1 L' D)) \<union> dom \<sigma>; extends_subst \<sigma> \<tau>; subst_cls (mset (remove1 L' D)) (subst_of_map Var \<tau>) \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. - L = subst_lit L' \<sigma> \<and> subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C
[PROOF STEP]
by (cases L; cases L'; auto simp add: subst_lit_def subst_of_map_def extends_subst_def
        dest!: match_term_list_sound intro!: exI[of _ "subst_of_map Var \<tau>"] term_subst_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_pos L'; is_pos L; \<not> False; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
 2. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for \<sigma> \<tau>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some \<sigma>; is_pos L'; is_pos L; \<not> False; - L = subst_lit L' \<tau>; subst_cls (mset (remove1 L' D)) \<tau> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (cases L; cases L'; simp add: subst_lit_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2 \<sigma>. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some x2; is_neg L; is_neg L'; - L = subst_lit L' \<sigma>; subst_cls (mset (remove1 L' D)) \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for \<sigma> \<tau>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D \<in> set Ds; L' \<in> set D; match_term_list [(atm_of L', atm_of L)] Map.empty = Some \<sigma>; is_neg L; is_neg L'; - L = subst_lit L' \<tau>; subst_cls (mset (remove1 L' D)) \<tau> \<subseteq># mset C\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (cases L; cases L'; simp add: subst_lit_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem prover_complete_refutation: "prover N \<longleftrightarrow> satisfiable (RP.grounded_N0 N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prover N = satisfiable (RP.grounded_N0 N)
[PROOF STEP]
unfolding prover_def St0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case deterministic_RP (RP.St0 N 0) of None \<Rightarrow> True | Some R \<Rightarrow> [] \<notin> set R) = satisfiable (RP.grounded_N0 N)
[PROOF STEP]
using RP.deterministic_RP_complete[of N 0] RP.deterministic_RP_refutation[of N 0]
[PROOF STATE]
proof (prove)
using this:
deterministic_RP (RP.St0 N 0) = None \<Longrightarrow> satisfiable (RP.grounded_N0 N)
deterministic_RP (RP.St0 N 0) = Some ?R \<Longrightarrow> (\<not> satisfiable (RP.grounded_N0 N)) = ({#} \<in> RP.grounded_R ?R)

goal (1 subgoal):
 1. (case deterministic_RP (RP.St0 N 0) of None \<Rightarrow> True | Some R \<Rightarrow> [] \<notin> set R) = satisfiable (RP.grounded_N0 N)
[PROOF STEP]
by (force simp: grounding_of_clss_def grounding_of_cls_def ex_ground_subst
    split: option.splits if_splits)


[STATEMENT]
lemma A_wb_prism [simp]: "wb_prism A\<^sub>\<triangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wb_prism A\<^sub>\<triangle>
[PROOF STEP]
using fromA.elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>fromA ?x = ?y; \<And>x. \<lbrakk>?x = A x; ?y = Some x\<rbrakk> \<Longrightarrow> ?P; \<And>v. \<lbrakk>?x = B v; ?y = None\<rbrakk> \<Longrightarrow> ?P; \<And>v. \<lbrakk>?x = C v; ?y = None\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. wb_prism A\<^sub>\<triangle>
[PROOF STEP]
by (unfold_locales, auto simp add: lens_defs)


[STATEMENT]
lemma B_wb_prism [simp]: "wb_prism B\<^sub>\<triangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wb_prism B\<^sub>\<triangle>
[PROOF STEP]
using fromB.elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>fromB ?x = ?y; \<And>x. \<lbrakk>?x = B x; ?y = Some x\<rbrakk> \<Longrightarrow> ?P; \<And>v. \<lbrakk>?x = A v; ?y = None\<rbrakk> \<Longrightarrow> ?P; \<And>v. \<lbrakk>?x = C v; ?y = None\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. wb_prism B\<^sub>\<triangle>
[PROOF STEP]
by (unfold_locales, auto simp add: lens_defs)


[STATEMENT]
lemma C_wb_prism [simp]: "wb_prism C\<^sub>\<triangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wb_prism C\<^sub>\<triangle>
[PROOF STEP]
using fromC.elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>fromC ?x = ?y; \<And>x. \<lbrakk>?x = C x; ?y = Some x\<rbrakk> \<Longrightarrow> ?P; \<And>v. \<lbrakk>?x = A v; ?y = None\<rbrakk> \<Longrightarrow> ?P; \<And>v. \<lbrakk>?x = B v; ?y = None\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. wb_prism C\<^sub>\<triangle>
[PROOF STEP]
by (unfold_locales, auto simp add: lens_defs)


[STATEMENT]
lemma D_codeps: "A\<^sub>\<triangle> \<nabla> B\<^sub>\<triangle>" "A\<^sub>\<triangle> \<nabla> C\<^sub>\<triangle>" "B\<^sub>\<triangle> \<nabla> C\<^sub>\<triangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sub>\<triangle> \<nabla> B\<^sub>\<triangle> &&& A\<^sub>\<triangle> \<nabla> C\<^sub>\<triangle> &&& B\<^sub>\<triangle> \<nabla> C\<^sub>\<triangle>
[PROOF STEP]
by (rule prism_diff_intro, simp add: lens_defs)+


[STATEMENT]
lemma unfold_eq_fix: "unfold\<cdot>h = fix\<cdot>(unfoldF\<cdot>h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unfold\<cdot>h = fix\<cdot>(unfoldF\<cdot>h)
[PROOF STEP]
proof (rule below_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. unfold\<cdot>h \<sqsubseteq> fix\<cdot>(unfoldF\<cdot>h)
 2. fix\<cdot>(unfoldF\<cdot>h) \<sqsubseteq> unfold\<cdot>h
[PROOF STEP]
show "unfold\<cdot>h \<sqsubseteq> fix\<cdot>(unfoldF\<cdot>h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unfold\<cdot>h \<sqsubseteq> fix\<cdot>(unfoldF\<cdot>h)
[PROOF STEP]
apply (rule unfold.induct, simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x\<cdot>h \<sqsubseteq> fix\<cdot>(unfoldF\<cdot>h) \<Longrightarrow> (\<Lambda> h v. Fixrec.run\<cdot>(match_bottom\<cdot>v\<cdot>(Fixrec.succeed\<cdot>\<bottom>) +++ Fixrec.succeed\<cdot>(case h\<cdot>v of Done \<Rightarrow> LNil | Skip\<cdot>s' \<Rightarrow> x\<cdot>h\<cdot>s' | Yield\<cdot>xa\<cdot>s' \<Rightarrow> LCons\<cdot>xa\<cdot>(x\<cdot>h\<cdot>s'))))\<cdot>h \<sqsubseteq> fix\<cdot>(unfoldF\<cdot>h)
[PROOF STEP]
apply (subst fix_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x\<cdot>h \<sqsubseteq> fix\<cdot>(unfoldF\<cdot>h) \<Longrightarrow> (\<Lambda> h v. Fixrec.run\<cdot>(match_bottom\<cdot>v\<cdot>(Fixrec.succeed\<cdot>\<bottom>) +++ Fixrec.succeed\<cdot>(Step_case\<cdot>LNil\<cdot>(Abs_cfun (Rep_cfun (x\<cdot>h)))\<cdot>(\<Lambda> xa s'. LCons\<cdot>xa\<cdot>(x\<cdot>h\<cdot>s'))\<cdot>(h\<cdot>v))))\<cdot>h \<sqsubseteq> unfoldF\<cdot>h\<cdot>(fix\<cdot>(unfoldF\<cdot>h))
[PROOF STEP]
apply (rule cfun_belowI, rename_tac s)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x s. x\<cdot>h \<sqsubseteq> fix\<cdot>(unfoldF\<cdot>h) \<Longrightarrow> (\<Lambda> h v. Fixrec.run\<cdot>(match_bottom\<cdot>v\<cdot>(Fixrec.succeed\<cdot>\<bottom>) +++ Fixrec.succeed\<cdot>(Step_case\<cdot>LNil\<cdot>(Abs_cfun (Rep_cfun (x\<cdot>h)))\<cdot>(\<Lambda> xa s'. LCons\<cdot>xa\<cdot>(x\<cdot>h\<cdot>s'))\<cdot>(h\<cdot>v))))\<cdot>h\<cdot>s \<sqsubseteq> unfoldF\<cdot>h\<cdot>(fix\<cdot>(unfoldF\<cdot>h))\<cdot>s
[PROOF STEP]
apply (case_tac "s = \<bottom>", simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>x\<cdot>h \<sqsubseteq> fix\<cdot>(unfoldF\<cdot>h); s \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Step_case\<cdot>LNil\<cdot>(Abs_cfun (Rep_cfun (x\<cdot>h)))\<cdot>(\<Lambda> xa s'. LCons\<cdot>xa\<cdot>(x\<cdot>h\<cdot>s'))\<cdot>(h\<cdot>s) \<sqsubseteq> (case h\<cdot>s of Done \<Rightarrow> LNil | Skip\<cdot>s' \<Rightarrow> fix\<cdot>(unfoldF\<cdot>h)\<cdot>s' | Yield\<cdot>x\<cdot>s' \<Rightarrow> LCons\<cdot>x\<cdot>(fix\<cdot>(unfoldF\<cdot>h)\<cdot>s'))
[PROOF STEP]
apply (intro monofun_cfun monofun_LAM below_refl, simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
unfold\<cdot>h \<sqsubseteq> fix\<cdot>(unfoldF\<cdot>h)

goal (1 subgoal):
 1. fix\<cdot>(unfoldF\<cdot>h) \<sqsubseteq> unfold\<cdot>h
[PROOF STEP]
show "fix\<cdot>(unfoldF\<cdot>h) \<sqsubseteq> unfold\<cdot>h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fix\<cdot>(unfoldF\<cdot>h) \<sqsubseteq> unfold\<cdot>h
[PROOF STEP]
apply (rule fix_ind, simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<sqsubseteq> unfold\<cdot>h \<Longrightarrow> unfoldF\<cdot>h\<cdot>x \<sqsubseteq> unfold\<cdot>h
[PROOF STEP]
apply (subst unfold.unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<sqsubseteq> unfold\<cdot>h \<Longrightarrow> unfoldF\<cdot>h\<cdot>x \<sqsubseteq> (\<Lambda> h v. Fixrec.run\<cdot>(match_bottom\<cdot>v\<cdot>(Fixrec.succeed\<cdot>\<bottom>) +++ Fixrec.succeed\<cdot>(Step_case\<cdot>LNil\<cdot>(Abs_cfun (Rep_cfun (unfold\<cdot>h)))\<cdot>(\<Lambda> x s'. LCons\<cdot>x\<cdot>(unfold\<cdot>h\<cdot>s'))\<cdot>(h\<cdot>v))))\<cdot>h
[PROOF STEP]
apply (rule cfun_belowI, rename_tac s)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x s. x \<sqsubseteq> unfold\<cdot>h \<Longrightarrow> unfoldF\<cdot>h\<cdot>x\<cdot>s \<sqsubseteq> (\<Lambda> h v. Fixrec.run\<cdot>(match_bottom\<cdot>v\<cdot>(Fixrec.succeed\<cdot>\<bottom>) +++ Fixrec.succeed\<cdot>(Step_case\<cdot>LNil\<cdot>(Abs_cfun (Rep_cfun (unfold\<cdot>h)))\<cdot>(\<Lambda> x s'. LCons\<cdot>x\<cdot>(unfold\<cdot>h\<cdot>s'))\<cdot>(h\<cdot>v))))\<cdot>h\<cdot>s
[PROOF STEP]
apply (case_tac "s = \<bottom>", simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>x \<sqsubseteq> unfold\<cdot>h; s \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (case h\<cdot>s of Done \<Rightarrow> LNil | Skip\<cdot>s' \<Rightarrow> x\<cdot>s' | Yield\<cdot>xa\<cdot>s' \<Rightarrow> LCons\<cdot>xa\<cdot>(x\<cdot>s')) \<sqsubseteq> Step_case\<cdot>LNil\<cdot>(Abs_cfun (Rep_cfun (unfold\<cdot>h)))\<cdot>(\<Lambda> x s'. LCons\<cdot>x\<cdot>(unfold\<cdot>h\<cdot>s'))\<cdot>(h\<cdot>s)
[PROOF STEP]
apply (intro monofun_cfun monofun_LAM below_refl, simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
fix\<cdot>(unfoldF\<cdot>h) \<sqsubseteq> unfold\<cdot>h

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unfold_ind:
    fixes P :: "('s \<rightarrow> 'a LList) \<Rightarrow> bool"
    assumes "adm P" and "P \<bottom>" and "\<And>u. P u \<Longrightarrow> P (unfoldF\<cdot>h\<cdot>u)"
    shows "P (unfold\<cdot>h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (unfold\<cdot>h)
[PROOF STEP]
unfolding unfold_eq_fix
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (fix\<cdot>(unfoldF\<cdot>h))
[PROOF STEP]
by (rule fix_ind [of P, OF assms])


[STATEMENT]
lemma unfold2_strict [simp]: "unfold2\<cdot>u\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unfold2\<cdot>u\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma unfold: "s \<noteq> \<bottom> \<Longrightarrow> unfold\<cdot>h\<cdot>s = unfold2\<cdot>(unfold\<cdot>h)\<cdot>(h\<cdot>s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> \<bottom> \<Longrightarrow> unfold\<cdot>h\<cdot>s = unfold2\<cdot>(unfold\<cdot>h)\<cdot>(h\<cdot>s)
[PROOF STEP]
by (case_tac "h\<cdot>s", simp_all)


[STATEMENT]
lemma unfoldF: "s \<noteq> \<bottom> \<Longrightarrow> unfoldF\<cdot>h\<cdot>u\<cdot>s = unfold2\<cdot>u\<cdot>(h\<cdot>s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> \<bottom> \<Longrightarrow> unfoldF\<cdot>h\<cdot>u\<cdot>s = unfold2\<cdot>u\<cdot>(h\<cdot>s)
[PROOF STEP]
by (case_tac "h\<cdot>s", simp_all)


[STATEMENT]
lemma unstream_strict [simp]: "unstream\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unstream\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma streamStep_strict [simp]: "streamStep\<cdot>(up\<cdot>\<bottom>) = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. streamStep\<cdot>(up\<cdot>\<bottom>) = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma stream_defined [simp]: "stream\<cdot>xs \<noteq> \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream\<cdot>xs \<noteq> \<bottom>
[PROOF STEP]
by simp


[STATEMENT]
lemma unstream_stream [simp]:
  fixes xs :: "'a LList"
  shows "unstream\<cdot>(stream\<cdot>xs) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unstream\<cdot>(stream\<cdot>xs) = xs
[PROOF STEP]
by (induct xs, simp_all add: unfold)


[STATEMENT]
lemma unstream_cong:
  "a \<approx> b \<Longrightarrow> unstream\<cdot>a = unstream\<cdot>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<approx> b \<Longrightarrow> unstream\<cdot>a = unstream\<cdot>b
[PROOF STEP]
unfolding bisimilar_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unstream\<cdot>a = unstream\<cdot>b \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom> \<Longrightarrow> unstream\<cdot>a = unstream\<cdot>b
[PROOF STEP]
by simp


[STATEMENT]
lemma stream_cong:
  "xs = ys \<Longrightarrow> stream\<cdot>xs \<approx> stream\<cdot>ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = ys \<Longrightarrow> stream\<cdot>xs \<approx> stream\<cdot>ys
[PROOF STEP]
unfolding bisimilar_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = ys \<Longrightarrow> unstream\<cdot>(stream\<cdot>xs) = unstream\<cdot>(stream\<cdot>ys) \<and> stream\<cdot>xs \<noteq> \<bottom> \<and> stream\<cdot>ys \<noteq> \<bottom>
[PROOF STEP]
by simp


[STATEMENT]
lemma stream_unstream_cong:
  "a \<approx> b \<Longrightarrow> stream\<cdot>(unstream\<cdot>a) \<approx> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<approx> b \<Longrightarrow> stream\<cdot>(unstream\<cdot>a) \<approx> b
[PROOF STEP]
unfolding bisimilar_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unstream\<cdot>a = unstream\<cdot>b \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom> \<Longrightarrow> unstream\<cdot>(stream\<cdot>(unstream\<cdot>a)) = unstream\<cdot>b \<and> stream\<cdot>(unstream\<cdot>a) \<noteq> \<bottom> \<and> b \<noteq> \<bottom>
[PROOF STEP]
by simp


[STATEMENT]
lemma tl_append_if: "tl (xs @ ys) = (if xs = [] then tl ys else tl xs @ ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (xs @ ys) = (if xs = [] then tl ys else tl xs @ ys)
[PROOF STEP]
by (simp)


[STATEMENT]
lemma take_last_length: "\<lbrakk>take (Suc 0) (rev xs) = [last xs]\<rbrakk> \<Longrightarrow> Suc 0 \<le> length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (Suc 0) (rev xs) = [last xs] \<Longrightarrow> Suc 0 \<le> length xs
[PROOF STEP]
by(induction xs) auto


[STATEMENT]
lemma take_last: "xs \<noteq> [] \<Longrightarrow> take 1 (rev xs) = [last xs]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> take 1 (rev xs) = [last xs]
[PROOF STEP]
by(induction xs)(auto simp: take_last_length)


[STATEMENT]
lemma take_hd [simp]: "xs \<noteq> [] \<Longrightarrow> take (Suc 0) xs = [hd xs]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> take (Suc 0) xs = [hd xs]
[PROOF STEP]
by(induction xs) auto


[STATEMENT]
lemma cons_tl: "x # xs = ys \<Longrightarrow> xs = tl ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x # xs = ys \<Longrightarrow> xs = tl ys
[PROOF STEP]
by auto


[STATEMENT]
lemma cons_hd: "x # xs = ys \<Longrightarrow> x = hd ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x # xs = ys \<Longrightarrow> x = hd ys
[PROOF STEP]
by auto


[STATEMENT]
lemma take_hd': "ys \<noteq> [] \<Longrightarrow> take (size ys) (x # xs) = take (Suc (size xs)) ys \<Longrightarrow> hd ys = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ys \<noteq> []; take (length ys) (x # xs) = take (Suc (length xs)) ys\<rbrakk> \<Longrightarrow> hd ys = x
[PROOF STEP]
by(induction ys) auto


[STATEMENT]
lemma rev_app_single: "rev xs @ [x] = rev (x # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev xs @ [x] = rev (x # xs)
[PROOF STEP]
by auto


[STATEMENT]
lemma hd_drop_1 [simp]: "xs \<noteq> [] \<Longrightarrow> hd xs # drop (Suc 0) xs = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> hd xs # drop (Suc 0) xs = xs
[PROOF STEP]
by(induction xs) auto


[STATEMENT]
lemma hd_drop [simp]: "n < length xs \<Longrightarrow> hd (drop n xs) # drop (Suc n) xs = drop n xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> hd (drop n xs) # drop (Suc n) xs = drop n xs
[PROOF STEP]
by(induction xs)(auto simp: list.expand tl_drop)


[STATEMENT]
lemma take_1: "0 < x \<and> 0 < y \<Longrightarrow> take x xs  = take y ys \<Longrightarrow> take 1 xs = take 1 ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < x \<and> 0 < y; take x xs = take y ys\<rbrakk> \<Longrightarrow> take 1 xs = take 1 ys
[PROOF STEP]
by (metis One_nat_def bot_nat_0.not_eq_extremum hd_take take_Suc take_eq_Nil)


[STATEMENT]
lemma last_drop_rev: "xs \<noteq> [] \<Longrightarrow> last xs # drop 1 (rev xs) = rev xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> last xs # drop 1 (rev xs) = rev xs
[PROOF STEP]
by (metis One_nat_def hd_drop_1 hd_rev rev.simps(1) rev_rev_ident)


[STATEMENT]
lemma Suc_min [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> Suc (min (x - Suc 0) (y - Suc 0)) = min x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> Suc (min (x - Suc 0) (y - Suc 0)) = min x y
[PROOF STEP]
by auto


[STATEMENT]
lemma rev_tl_hd: "xs \<noteq> [] \<Longrightarrow> rev (tl xs) @ [hd xs] = rev xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> rev (tl xs) @ [hd xs] = rev xs
[PROOF STEP]
by (simp add: rev_app_single)


[STATEMENT]
lemma app_rev: "as @ rev bs = cs @ rev ds \<Longrightarrow> bs @ rev as = ds @ rev cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. as @ rev bs = cs @ rev ds \<Longrightarrow> bs @ rev as = ds @ rev cs
[PROOF STEP]
by (metis rev_append rev_rev_ident)


[STATEMENT]
lemma tl_drop_2: "tl (drop n xs) = drop (Suc n) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (drop n xs) = drop (Suc n) xs
[PROOF STEP]
by (simp add: drop_Suc tl_drop)


[STATEMENT]
lemma Suc_sub: "Suc n = m \<Longrightarrow> n = m - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc n = m \<Longrightarrow> n = m - 1
[PROOF STEP]
by simp


[STATEMENT]
lemma length_one_hd: "length xs = 1 \<Longrightarrow> xs = [hd xs]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = 1 \<Longrightarrow> xs = [hd xs]
[PROOF STEP]
by(induction xs) auto


[STATEMENT]
theorem HCSCND:
  defines "hc F \<equiv> AX10 \<turnstile>\<^sub>H F"
  defines "nd F \<equiv> {} \<turnstile> F"
  defines "sc F \<equiv> {#} \<Rightarrow> {# F #}"
  shows "hc F \<longleftrightarrow> nd F" and "nd F \<longleftrightarrow> sc F" and "sc F \<longleftrightarrow> hc F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hc F = nd F &&& nd F = sc F &&& sc F = hc F
[PROOF STEP]
using HCSC[where F=F and \<Gamma>=\<open>{#}\<close>, simplified]
      SCND[where \<Gamma>=\<open>{#}\<close> and \<Delta>="{#F#}"] ND.ND.CC[where F=F and \<Gamma>="{}"]
      NDHC[where \<Gamma>="{}" and F=F]
[PROOF STATE]
proof (prove)
using this:
AX10 \<turnstile>\<^sub>H F \<Longrightarrow> {#} \<Rightarrow> F, {#}
{#} \<Rightarrow> F, {#} \<Longrightarrow> set_mset {#} \<union> \<^bold>\<not> ` set_mset (F, {#}) \<turnstile> \<bottom>
{\<^bold>\<not> F} \<turnstile> \<bottom> \<Longrightarrow> {} \<turnstile> F
{} \<turnstile> F \<Longrightarrow> AX10 \<union> {} \<turnstile>\<^sub>H F

goal (1 subgoal):
 1. hc F = nd F &&& nd F = sc F &&& sc F = hc F
[PROOF STEP]
by(simp_all add: assms) blast+


[STATEMENT]
lemma af_decompose:
  "af (\<phi> and \<psi>) w = (af \<phi> w) and (af \<psi> w)"
  "af (\<phi> or \<psi>) w = (af \<phi> w) or (af \<psi> w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af (\<phi> and \<psi>) w = af \<phi> w and af \<psi> w &&& af (\<phi> or \<psi>) w = af \<phi> w or af \<psi> w
[PROOF STEP]
by (induction w rule: rev_induct) simp_all


[STATEMENT]
lemma af_simps[simp]:
  "af true w = true"
  "af false w = false"
  "af (X \<phi>) (x#xs) = af \<phi> (xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af true w = true &&& af false w = false &&& af (X \<phi>) (x # xs) = af \<phi> xs
[PROOF STEP]
by (induction w) simp_all


[STATEMENT]
lemma af_F:
  "af (F \<phi>) w = Or (F \<phi> # map (af \<phi>) (suffixes w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af (F \<phi>) w = Or (F \<phi> # map (af \<phi>) (suffixes w))
[PROOF STEP]
proof (induction w)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. af (F \<phi>) [] = Or (F \<phi> # map (af \<phi>) (suffixes []))
 2. \<And>a w. af (F \<phi>) w = Or (F \<phi> # map (af \<phi>) (suffixes w)) \<Longrightarrow> af (F \<phi>) (a # w) = Or (F \<phi> # map (af \<phi>) (suffixes (a # w)))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
af (F \<phi>) xs = Or (F \<phi> # map (af \<phi>) (suffixes xs))

goal (2 subgoals):
 1. af (F \<phi>) [] = Or (F \<phi> # map (af \<phi>) (suffixes []))
 2. \<And>a w. af (F \<phi>) w = Or (F \<phi> # map (af \<phi>) (suffixes w)) \<Longrightarrow> af (F \<phi>) (a # w) = Or (F \<phi> # map (af \<phi>) (suffixes (a # w)))
[PROOF STEP]
have "af (F \<phi>) (x # xs) = af (af_letter (F \<phi>) x) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af (F \<phi>) (x # xs) = af (af_letter (F \<phi>) x) xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
af (F \<phi>) (x # xs) = af (af_letter (F \<phi>) x) xs

goal (2 subgoals):
 1. af (F \<phi>) [] = Or (F \<phi> # map (af \<phi>) (suffixes []))
 2. \<And>a w. af (F \<phi>) w = Or (F \<phi> # map (af \<phi>) (suffixes w)) \<Longrightarrow> af (F \<phi>) (a # w) = Or (F \<phi> # map (af \<phi>) (suffixes (a # w)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
af (F \<phi>) (x # xs) = af (af_letter (F \<phi>) x) xs

goal (2 subgoals):
 1. af (F \<phi>) [] = Or (F \<phi> # map (af \<phi>) (suffixes []))
 2. \<And>a w. af (F \<phi>) w = Or (F \<phi> # map (af \<phi>) (suffixes w)) \<Longrightarrow> af (F \<phi>) (a # w) = Or (F \<phi> # map (af \<phi>) (suffixes (a # w)))
[PROOF STEP]
have "\<dots> = (af (F \<phi>) xs) or (af (af_letter (\<phi>) x) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af (af_letter (F \<phi>) x) xs = af (F \<phi>) xs or af (af_letter \<phi> x) xs
[PROOF STEP]
unfolding af_decompose[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af (af_letter (F \<phi>) x) xs = af (F \<phi> or af_letter \<phi> x) xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
af (af_letter (F \<phi>) x) xs = af (F \<phi>) xs or af (af_letter \<phi> x) xs

goal (2 subgoals):
 1. af (F \<phi>) [] = Or (F \<phi> # map (af \<phi>) (suffixes []))
 2. \<And>a w. af (F \<phi>) w = Or (F \<phi> # map (af \<phi>) (suffixes w)) \<Longrightarrow> af (F \<phi>) (a # w) = Or (F \<phi> # map (af \<phi>) (suffixes (a # w)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
af (F \<phi>) (x # xs) = af (F \<phi>) xs or af (af_letter \<phi> x) xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
af (F \<phi>) (x # xs) = af (F \<phi>) xs or af (af_letter \<phi> x) xs

goal (1 subgoal):
 1. af (F \<phi>) (x # xs) = Or (F \<phi> # map (af \<phi>) (suffixes (x # xs)))
[PROOF STEP]
using Cons Or_append_syntactic
[PROOF STATE]
proof (prove)
using this:
af (F \<phi>) (x # xs) = af (F \<phi>) xs or af (af_letter \<phi> x) xs
af (F \<phi>) xs = Or (F \<phi> # map (af \<phi>) (suffixes xs))
?xs \<noteq> [] \<Longrightarrow> Or (?xs @ ?ys) = Or (Or ?xs # ?ys)

goal (1 subgoal):
 1. af (F \<phi>) (x # xs) = Or (F \<phi> # map (af \<phi>) (suffixes (x # xs)))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
af (F \<phi>) (x # xs) = Or (F \<phi> # map (af \<phi>) (suffixes (x # xs)))

goal (1 subgoal):
 1. af (F \<phi>) [] = Or (F \<phi> # map (af \<phi>) (suffixes []))
[PROOF STEP]
qed simp


[STATEMENT]
lemma af_G:
  "af (G \<phi>) w = And (G \<phi> # map (af \<phi>) (suffixes w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af (G \<phi>) w = And (G \<phi> # map (af \<phi>) (suffixes w))
[PROOF STEP]
proof (induction w)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. af (G \<phi>) [] = And (G \<phi> # map (af \<phi>) (suffixes []))
 2. \<And>a w. af (G \<phi>) w = And (G \<phi> # map (af \<phi>) (suffixes w)) \<Longrightarrow> af (G \<phi>) (a # w) = And (G \<phi> # map (af \<phi>) (suffixes (a # w)))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
af (G \<phi>) xs = And (G \<phi> # map (af \<phi>) (suffixes xs))

goal (2 subgoals):
 1. af (G \<phi>) [] = And (G \<phi> # map (af \<phi>) (suffixes []))
 2. \<And>a w. af (G \<phi>) w = And (G \<phi> # map (af \<phi>) (suffixes w)) \<Longrightarrow> af (G \<phi>) (a # w) = And (G \<phi> # map (af \<phi>) (suffixes (a # w)))
[PROOF STEP]
have "af (G \<phi>) (x # xs) = af (af_letter (G \<phi>) x) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af (G \<phi>) (x # xs) = af (af_letter (G \<phi>) x) xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
af (G \<phi>) (x # xs) = af (af_letter (G \<phi>) x) xs

goal (2 subgoals):
 1. af (G \<phi>) [] = And (G \<phi> # map (af \<phi>) (suffixes []))
 2. \<And>a w. af (G \<phi>) w = And (G \<phi> # map (af \<phi>) (suffixes w)) \<Longrightarrow> af (G \<phi>) (a # w) = And (G \<phi> # map (af \<phi>) (suffixes (a # w)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
af (G \<phi>) (x # xs) = af (af_letter (G \<phi>) x) xs

goal (2 subgoals):
 1. af (G \<phi>) [] = And (G \<phi> # map (af \<phi>) (suffixes []))
 2. \<And>a w. af (G \<phi>) w = And (G \<phi> # map (af \<phi>) (suffixes w)) \<Longrightarrow> af (G \<phi>) (a # w) = And (G \<phi> # map (af \<phi>) (suffixes (a # w)))
[PROOF STEP]
have "\<dots> = (af (G \<phi>) xs) and (af (af_letter (\<phi>) x) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af (af_letter (G \<phi>) x) xs = af (G \<phi>) xs and af (af_letter \<phi> x) xs
[PROOF STEP]
unfolding af_decompose[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af (af_letter (G \<phi>) x) xs = af (G \<phi> and af_letter \<phi> x) xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
af (af_letter (G \<phi>) x) xs = af (G \<phi>) xs and af (af_letter \<phi> x) xs

goal (2 subgoals):
 1. af (G \<phi>) [] = And (G \<phi> # map (af \<phi>) (suffixes []))
 2. \<And>a w. af (G \<phi>) w = And (G \<phi> # map (af \<phi>) (suffixes w)) \<Longrightarrow> af (G \<phi>) (a # w) = And (G \<phi> # map (af \<phi>) (suffixes (a # w)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
af (G \<phi>) (x # xs) = af (G \<phi>) xs and af (af_letter \<phi> x) xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
af (G \<phi>) (x # xs) = af (G \<phi>) xs and af (af_letter \<phi> x) xs

goal (1 subgoal):
 1. af (G \<phi>) (x # xs) = And (G \<phi> # map (af \<phi>) (suffixes (x # xs)))
[PROOF STEP]
using Cons Or_append_syntactic
[PROOF STATE]
proof (prove)
using this:
af (G \<phi>) (x # xs) = af (G \<phi>) xs and af (af_letter \<phi> x) xs
af (G \<phi>) xs = And (G \<phi> # map (af \<phi>) (suffixes xs))
?xs \<noteq> [] \<Longrightarrow> Or (?xs @ ?ys) = Or (Or ?xs # ?ys)

goal (1 subgoal):
 1. af (G \<phi>) (x # xs) = And (G \<phi> # map (af \<phi>) (suffixes (x # xs)))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
af (G \<phi>) (x # xs) = And (G \<phi> # map (af \<phi>) (suffixes (x # xs)))

goal (1 subgoal):
 1. af (G \<phi>) [] = And (G \<phi> # map (af \<phi>) (suffixes []))
[PROOF STEP]
qed simp


[STATEMENT]
lemma af_U:
  "af (\<phi> U \<psi>) (x#xs) = (af (\<phi> U \<psi>) xs and af \<phi> (x#xs)) or af \<psi> (x#xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af (\<phi> U \<psi>) (x # xs) = af (\<phi> U \<psi>) xs and af \<phi> (x # xs) or af \<psi> (x # xs)
[PROOF STEP]
by (induction xs) (simp add: af_decompose)+


[STATEMENT]
lemma af_respectfulness:
  "\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter \<psi> \<nu>"
  "\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<equiv>\<^sub>P af_letter \<psi> \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<equiv>\<^sub>P af_letter \<psi> \<nu>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter \<psi> \<nu>
 2. \<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<equiv>\<^sub>P af_letter \<psi> \<nu>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter \<psi> \<nu>
 2. \<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<equiv>\<^sub>P af_letter \<psi> \<nu>
[PROOF STEP]
fix \<phi>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter \<psi> \<nu>
 2. \<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<equiv>\<^sub>P af_letter \<psi> \<nu>
[PROOF STEP]
have "af_letter \<phi> \<nu> = subst \<phi> (\<lambda>\<chi>. Some (af_letter \<chi> \<nu>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af_letter \<phi> \<nu> = subst \<phi> (\<lambda>\<chi>. Some (af_letter \<chi> \<nu>))
[PROOF STEP]
by (induction \<phi>) auto
[PROOF STATE]
proof (state)
this:
af_letter \<phi> \<nu> = subst \<phi> (\<lambda>\<chi>. Some (af_letter \<chi> \<nu>))

goal (2 subgoals):
 1. \<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter \<psi> \<nu>
 2. \<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<equiv>\<^sub>P af_letter \<psi> \<nu>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
af_letter ?\<phi>'2 \<nu> = subst ?\<phi>'2 (\<lambda>\<chi>. Some (af_letter \<chi> \<nu>))

goal (2 subgoals):
 1. \<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter \<psi> \<nu>
 2. \<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<equiv>\<^sub>P af_letter \<psi> \<nu>
[PROOF STEP]
thus "\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter \<psi> \<nu>"
    and "\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<equiv>\<^sub>P af_letter \<psi> \<nu>"
[PROOF STATE]
proof (prove)
using this:
af_letter ?\<phi>'2 \<nu> = subst ?\<phi>'2 (\<lambda>\<chi>. Some (af_letter \<chi> \<nu>))

goal (1 subgoal):
 1. (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<equiv>\<^sub>P af_letter \<psi> \<nu>)
[PROOF STEP]
using subst_respects_ltl_prop_entailment
[PROOF STATE]
proof (prove)
using this:
af_letter ?\<phi>'2 \<nu> = subst ?\<phi>'2 (\<lambda>\<chi>. Some (af_letter \<chi> \<nu>))
?\<phi> \<longrightarrow>\<^sub>P ?\<psi> \<Longrightarrow> subst ?\<phi> ?m \<longrightarrow>\<^sub>P subst ?\<psi> ?m
?\<phi> \<equiv>\<^sub>P ?\<psi> \<Longrightarrow> subst ?\<phi> ?m \<equiv>\<^sub>P subst ?\<psi> ?m

goal (1 subgoal):
 1. (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<equiv>\<^sub>P af_letter \<psi> \<nu>)
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_letter \<psi> \<nu>
\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_letter \<phi> \<nu> \<equiv>\<^sub>P af_letter \<psi> \<nu>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma af_respectfulness':
  "\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af \<phi> w \<longrightarrow>\<^sub>P af \<psi> w"
  "\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af \<phi> w \<equiv>\<^sub>P af \<psi> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af \<phi> w \<longrightarrow>\<^sub>P af \<psi> w) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af \<phi> w \<equiv>\<^sub>P af \<psi> w)
[PROOF STEP]
by (induction w arbitrary: \<phi> \<psi>) (insert af_respectfulness, fastforce+)


[STATEMENT]
lemma af_nested_propos:
  "nested_propos (af_letter \<phi> \<nu>) \<subseteq> nested_propos \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nested_propos (af_letter \<phi> \<nu>) \<subseteq> nested_propos \<phi>
[PROOF STEP]
by (induction \<phi>) auto


[STATEMENT]
lemma af\<^sub>G_decompose:
  "af\<^sub>G (\<phi> and \<psi>) w = (af\<^sub>G \<phi> w) and (af\<^sub>G \<psi> w)"
  "af\<^sub>G (\<phi> or \<psi>) w = (af\<^sub>G \<phi> w) or (af\<^sub>G \<psi> w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af\<^sub>G (\<phi> and \<psi>) w = af\<^sub>G \<phi> w and af\<^sub>G \<psi> w &&& af\<^sub>G (\<phi> or \<psi>) w = af\<^sub>G \<phi> w or af\<^sub>G \<psi> w
[PROOF STEP]
by (induction w rule: rev_induct) simp_all


[STATEMENT]
lemma af\<^sub>G_simps[simp]:
  "af\<^sub>G true w = true"
  "af\<^sub>G false w = false"
  "af\<^sub>G (G \<phi>) w = G \<phi>"
  "af\<^sub>G (X \<phi>) (x#xs) = af\<^sub>G \<phi> (xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (af\<^sub>G true w = true &&& af\<^sub>G false w = false) &&& af\<^sub>G (G \<phi>) w = G \<phi> &&& af\<^sub>G (X \<phi>) (x # xs) = af\<^sub>G \<phi> xs
[PROOF STEP]
by (induction w) simp_all


[STATEMENT]
lemma af\<^sub>G_F:
  "af\<^sub>G (F \<phi>) w = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af\<^sub>G (F \<phi>) w = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes w))
[PROOF STEP]
proof (induction w)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. af\<^sub>G (F \<phi>) [] = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes []))
 2. \<And>a w. af\<^sub>G (F \<phi>) w = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes w)) \<Longrightarrow> af\<^sub>G (F \<phi>) (a # w) = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes (a # w)))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
af\<^sub>G (F \<phi>) xs = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes xs))

goal (2 subgoals):
 1. af\<^sub>G (F \<phi>) [] = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes []))
 2. \<And>a w. af\<^sub>G (F \<phi>) w = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes w)) \<Longrightarrow> af\<^sub>G (F \<phi>) (a # w) = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes (a # w)))
[PROOF STEP]
have "af\<^sub>G (F \<phi>) (x # xs) = af\<^sub>G (af_G_letter (F \<phi>) x) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af\<^sub>G (F \<phi>) (x # xs) = af\<^sub>G (af_G_letter (F \<phi>) x) xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
af\<^sub>G (F \<phi>) (x # xs) = af\<^sub>G (af_G_letter (F \<phi>) x) xs

goal (2 subgoals):
 1. af\<^sub>G (F \<phi>) [] = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes []))
 2. \<And>a w. af\<^sub>G (F \<phi>) w = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes w)) \<Longrightarrow> af\<^sub>G (F \<phi>) (a # w) = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes (a # w)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
af\<^sub>G (F \<phi>) (x # xs) = af\<^sub>G (af_G_letter (F \<phi>) x) xs

goal (2 subgoals):
 1. af\<^sub>G (F \<phi>) [] = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes []))
 2. \<And>a w. af\<^sub>G (F \<phi>) w = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes w)) \<Longrightarrow> af\<^sub>G (F \<phi>) (a # w) = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes (a # w)))
[PROOF STEP]
have "\<dots> = (af\<^sub>G (F \<phi>) xs) or (af\<^sub>G (af_G_letter (\<phi>) x) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af\<^sub>G (af_G_letter (F \<phi>) x) xs = af\<^sub>G (F \<phi>) xs or af\<^sub>G (af_G_letter \<phi> x) xs
[PROOF STEP]
unfolding af\<^sub>G_decompose[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af\<^sub>G (af_G_letter (F \<phi>) x) xs = af\<^sub>G (F \<phi> or af_G_letter \<phi> x) xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
af\<^sub>G (af_G_letter (F \<phi>) x) xs = af\<^sub>G (F \<phi>) xs or af\<^sub>G (af_G_letter \<phi> x) xs

goal (2 subgoals):
 1. af\<^sub>G (F \<phi>) [] = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes []))
 2. \<And>a w. af\<^sub>G (F \<phi>) w = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes w)) \<Longrightarrow> af\<^sub>G (F \<phi>) (a # w) = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes (a # w)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
af\<^sub>G (F \<phi>) (x # xs) = af\<^sub>G (F \<phi>) xs or af\<^sub>G (af_G_letter \<phi> x) xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
af\<^sub>G (F \<phi>) (x # xs) = af\<^sub>G (F \<phi>) xs or af\<^sub>G (af_G_letter \<phi> x) xs

goal (1 subgoal):
 1. af\<^sub>G (F \<phi>) (x # xs) = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes (x # xs)))
[PROOF STEP]
using Cons Or_append_syntactic
[PROOF STATE]
proof (prove)
using this:
af\<^sub>G (F \<phi>) (x # xs) = af\<^sub>G (F \<phi>) xs or af\<^sub>G (af_G_letter \<phi> x) xs
af\<^sub>G (F \<phi>) xs = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes xs))
?xs \<noteq> [] \<Longrightarrow> Or (?xs @ ?ys) = Or (Or ?xs # ?ys)

goal (1 subgoal):
 1. af\<^sub>G (F \<phi>) (x # xs) = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes (x # xs)))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
af\<^sub>G (F \<phi>) (x # xs) = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes (x # xs)))

goal (1 subgoal):
 1. af\<^sub>G (F \<phi>) [] = Or (F \<phi> # map (af\<^sub>G \<phi>) (suffixes []))
[PROOF STEP]
qed simp


[STATEMENT]
lemma af\<^sub>G_U:
  "af\<^sub>G (\<phi> U \<psi>) (x#xs) = (af\<^sub>G (\<phi> U \<psi>) xs and af\<^sub>G \<phi> (x#xs)) or af\<^sub>G \<psi> (x#xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af\<^sub>G (\<phi> U \<psi>) (x # xs) = af\<^sub>G (\<phi> U \<psi>) xs and af\<^sub>G \<phi> (x # xs) or af\<^sub>G \<psi> (x # xs)
[PROOF STEP]
by (simp add: af\<^sub>G_decompose)


[STATEMENT]
lemma af\<^sub>G_subsequence_U:
  "af\<^sub>G (\<phi> U \<psi>) (w [0 \<rightarrow> Suc n]) = (af\<^sub>G (\<phi> U \<psi>) (w [1 \<rightarrow> Suc n]) and af\<^sub>G \<phi> (w [0 \<rightarrow> Suc n])) or af\<^sub>G \<psi> (w [0 \<rightarrow> Suc n])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af\<^sub>G (\<phi> U \<psi>) (prefix (Suc n) w) = af\<^sub>G (\<phi> U \<psi>) (w [1 \<rightarrow> Suc n]) and af\<^sub>G \<phi> (prefix (Suc n) w) or af\<^sub>G \<psi> (prefix (Suc n) w)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. af\<^sub>G (\<phi> U \<psi>) (prefix (Suc n) w) = af\<^sub>G (\<phi> U \<psi>) (w [1 \<rightarrow> Suc n]) and af\<^sub>G \<phi> (prefix (Suc n) w) or af\<^sub>G \<psi> (prefix (Suc n) w)
[PROOF STEP]
have "\<And>n. w [0 \<rightarrow> Suc n] = w 0 # w [1 \<rightarrow> Suc n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. prefix (Suc n) w = w 0 # w [1 \<rightarrow> Suc n]
[PROOF STEP]
using subsequence_append[of w 1]
[PROOF STATE]
proof (prove)
using this:
prefix (1 + ?j) w = prefix 1 w @ w [1 \<rightarrow> 1 + ?j]

goal (1 subgoal):
 1. \<And>n. prefix (Suc n) w = w 0 # w [1 \<rightarrow> Suc n]
[PROOF STEP]
by (simp add: subsequence_def upt_conv_Cons)
[PROOF STATE]
proof (state)
this:
prefix (Suc ?n) w = w 0 # w [1 \<rightarrow> Suc ?n]

goal (1 subgoal):
 1. af\<^sub>G (\<phi> U \<psi>) (prefix (Suc n) w) = af\<^sub>G (\<phi> U \<psi>) (w [1 \<rightarrow> Suc n]) and af\<^sub>G \<phi> (prefix (Suc n) w) or af\<^sub>G \<psi> (prefix (Suc n) w)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
prefix (Suc ?n) w = w 0 # w [1 \<rightarrow> Suc ?n]

goal (1 subgoal):
 1. af\<^sub>G (\<phi> U \<psi>) (prefix (Suc n) w) = af\<^sub>G (\<phi> U \<psi>) (w [1 \<rightarrow> Suc n]) and af\<^sub>G \<phi> (prefix (Suc n) w) or af\<^sub>G \<psi> (prefix (Suc n) w)
[PROOF STEP]
using af\<^sub>G_U
[PROOF STATE]
proof (prove)
using this:
prefix (Suc ?n) w = w 0 # w [1 \<rightarrow> Suc ?n]
af\<^sub>G (?\<phi> U ?\<psi>) (?x # ?xs) = af\<^sub>G (?\<phi> U ?\<psi>) ?xs and af\<^sub>G ?\<phi> (?x # ?xs) or af\<^sub>G ?\<psi> (?x # ?xs)

goal (1 subgoal):
 1. af\<^sub>G (\<phi> U \<psi>) (prefix (Suc n) w) = af\<^sub>G (\<phi> U \<psi>) (w [1 \<rightarrow> Suc n]) and af\<^sub>G \<phi> (prefix (Suc n) w) or af\<^sub>G \<psi> (prefix (Suc n) w)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
af\<^sub>G (\<phi> U \<psi>) (prefix (Suc n) w) = af\<^sub>G (\<phi> U \<psi>) (w [1 \<rightarrow> Suc n]) and af\<^sub>G \<phi> (prefix (Suc n) w) or af\<^sub>G \<psi> (prefix (Suc n) w)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma af_G_respectfulness:
  "\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter \<psi> \<nu>"
  "\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<equiv>\<^sub>P af_G_letter \<psi> \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<equiv>\<^sub>P af_G_letter \<psi> \<nu>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter \<psi> \<nu>
 2. \<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<equiv>\<^sub>P af_G_letter \<psi> \<nu>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter \<psi> \<nu>
 2. \<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<equiv>\<^sub>P af_G_letter \<psi> \<nu>
[PROOF STEP]
fix \<phi>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter \<psi> \<nu>
 2. \<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<equiv>\<^sub>P af_G_letter \<psi> \<nu>
[PROOF STEP]
have "af_G_letter \<phi> \<nu> = subst \<phi> (\<lambda>\<chi>. Some (af_G_letter \<chi> \<nu>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af_G_letter \<phi> \<nu> = subst \<phi> (\<lambda>\<chi>. Some (af_G_letter \<chi> \<nu>))
[PROOF STEP]
by (induction \<phi>) auto
[PROOF STATE]
proof (state)
this:
af_G_letter \<phi> \<nu> = subst \<phi> (\<lambda>\<chi>. Some (af_G_letter \<chi> \<nu>))

goal (2 subgoals):
 1. \<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter \<psi> \<nu>
 2. \<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<equiv>\<^sub>P af_G_letter \<psi> \<nu>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
af_G_letter ?\<phi>'2 \<nu> = subst ?\<phi>'2 (\<lambda>\<chi>. Some (af_G_letter \<chi> \<nu>))

goal (2 subgoals):
 1. \<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter \<psi> \<nu>
 2. \<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<equiv>\<^sub>P af_G_letter \<psi> \<nu>
[PROOF STEP]
thus "\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter \<psi> \<nu>"
    and "\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<equiv>\<^sub>P af_G_letter \<psi> \<nu>"
[PROOF STATE]
proof (prove)
using this:
af_G_letter ?\<phi>'2 \<nu> = subst ?\<phi>'2 (\<lambda>\<chi>. Some (af_G_letter \<chi> \<nu>))

goal (1 subgoal):
 1. (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<equiv>\<^sub>P af_G_letter \<psi> \<nu>)
[PROOF STEP]
using subst_respects_ltl_prop_entailment
[PROOF STATE]
proof (prove)
using this:
af_G_letter ?\<phi>'2 \<nu> = subst ?\<phi>'2 (\<lambda>\<chi>. Some (af_G_letter \<chi> \<nu>))
?\<phi> \<longrightarrow>\<^sub>P ?\<psi> \<Longrightarrow> subst ?\<phi> ?m \<longrightarrow>\<^sub>P subst ?\<psi> ?m
?\<phi> \<equiv>\<^sub>P ?\<psi> \<Longrightarrow> subst ?\<phi> ?m \<equiv>\<^sub>P subst ?\<psi> ?m

goal (1 subgoal):
 1. (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter \<psi> \<nu>) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<equiv>\<^sub>P af_G_letter \<psi> \<nu>)
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<longrightarrow>\<^sub>P af_G_letter \<psi> \<nu>
\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af_G_letter \<phi> \<nu> \<equiv>\<^sub>P af_G_letter \<psi> \<nu>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma af_G_respectfulness':
  "\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af\<^sub>G \<phi> w \<longrightarrow>\<^sub>P af\<^sub>G \<psi> w"
  "\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af\<^sub>G \<phi> w \<equiv>\<^sub>P af\<^sub>G \<psi> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<phi> \<longrightarrow>\<^sub>P \<psi> \<Longrightarrow> af\<^sub>G \<phi> w \<longrightarrow>\<^sub>P af\<^sub>G \<psi> w) &&& (\<phi> \<equiv>\<^sub>P \<psi> \<Longrightarrow> af\<^sub>G \<phi> w \<equiv>\<^sub>P af\<^sub>G \<psi> w)
[PROOF STEP]
by (induction w arbitrary: \<phi> \<psi>) (insert af_G_respectfulness, fastforce+)


[STATEMENT]
lemma af_G_nested_propos:
  "nested_propos (af_G_letter \<phi> \<nu>) \<subseteq> nested_propos \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nested_propos (af_G_letter \<phi> \<nu>) \<subseteq> nested_propos \<phi>
[PROOF STEP]
by (induction \<phi>) auto


[STATEMENT]
lemma af_G_letter_sat_core:
  "Only_G \<G> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P \<phi> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P af_G_letter \<phi> \<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Only_G \<G>; \<G> \<Turnstile>\<^sub>P \<phi>\<rbrakk> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P af_G_letter \<phi> \<nu>
[PROOF STEP]
by (induction \<phi>) (simp_all, blast+)


[STATEMENT]
lemma af\<^sub>G_sat_core:
  "Only_G \<G> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P \<phi> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P af\<^sub>G \<phi> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Only_G \<G>; \<G> \<Turnstile>\<^sub>P \<phi>\<rbrakk> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P af\<^sub>G \<phi> w
[PROOF STEP]
using af_G_letter_sat_core
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Only_G ?\<G>; ?\<G> \<Turnstile>\<^sub>P ?\<phi>\<rbrakk> \<Longrightarrow> ?\<G> \<Turnstile>\<^sub>P af_G_letter ?\<phi> ?\<nu>

goal (1 subgoal):
 1. \<lbrakk>Only_G \<G>; \<G> \<Turnstile>\<^sub>P \<phi>\<rbrakk> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P af\<^sub>G \<phi> w
[PROOF STEP]
by (induction w rule: rev_induct) (simp_all, blast)


[STATEMENT]
lemma af\<^sub>G_sat_core_generalized:
  "Only_G \<G> \<Longrightarrow> i \<le> j \<Longrightarrow> \<G> \<Turnstile>\<^sub>P af\<^sub>G \<phi> (w [0 \<rightarrow> i]) \<Longrightarrow> \<G> \<Turnstile>\<^sub>P af\<^sub>G \<phi> (w [0 \<rightarrow> j])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Only_G \<G>; i \<le> j; \<G> \<Turnstile>\<^sub>P af\<^sub>G \<phi> (prefix i w)\<rbrakk> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P af\<^sub>G \<phi> (prefix j w)
[PROOF STEP]
by (metis af\<^sub>G_sat_core foldl_append subsequence_append le_add_diff_inverse)


[STATEMENT]
lemma af\<^sub>G_eval\<^sub>G:
  "Only_G \<G> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P af\<^sub>G (eval\<^sub>G \<G> \<phi>) w \<longleftrightarrow> \<G> \<Turnstile>\<^sub>P eval\<^sub>G \<G> (af\<^sub>G \<phi> w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Only_G \<G> \<Longrightarrow> \<G> \<Turnstile>\<^sub>P af\<^sub>G (eval\<^sub>G \<G> \<phi>) w = \<G> \<Turnstile>\<^sub>P eval\<^sub>G \<G> (af\<^sub>G \<phi> w)
[PROOF STEP]
by (induction \<phi>) (simp_all add: eval\<^sub>G_prop_entailment af\<^sub>G_decompose)


[STATEMENT]
lemma af\<^sub>G_keeps_F_and_S:
  assumes "ys \<noteq> []"
  assumes "S \<Turnstile>\<^sub>P af\<^sub>G \<phi> ys"
  shows "S \<Turnstile>\<^sub>P af\<^sub>G (F \<phi>) (xs @ ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<Turnstile>\<^sub>P af\<^sub>G (F \<phi>) (xs @ ys)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S \<Turnstile>\<^sub>P af\<^sub>G (F \<phi>) (xs @ ys)
[PROOF STEP]
have "af\<^sub>G \<phi> ys \<in> set (map (af\<^sub>G \<phi>) (suffixes (xs @ ys)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af\<^sub>G \<phi> ys \<in> set (map (af\<^sub>G \<phi>) (suffixes (xs @ ys)))
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> []

goal (1 subgoal):
 1. af\<^sub>G \<phi> ys \<in> set (map (af\<^sub>G \<phi>) (suffixes (xs @ ys)))
[PROOF STEP]
unfolding suffixes_append map_append
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> []

goal (1 subgoal):
 1. af\<^sub>G \<phi> ys \<in> set (map (af\<^sub>G \<phi>) (suffixes ys) @ map (af\<^sub>G \<phi>) (map (\<lambda>zs. zs @ ys) (suffixes xs)))
[PROOF STEP]
by (induction ys rule: List.list_nonempty_induct) auto
[PROOF STATE]
proof (state)
this:
af\<^sub>G \<phi> ys \<in> set (map (af\<^sub>G \<phi>) (suffixes (xs @ ys)))

goal (1 subgoal):
 1. S \<Turnstile>\<^sub>P af\<^sub>G (F \<phi>) (xs @ ys)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
af\<^sub>G \<phi> ys \<in> set (map (af\<^sub>G \<phi>) (suffixes (xs @ ys)))

goal (1 subgoal):
 1. S \<Turnstile>\<^sub>P af\<^sub>G (F \<phi>) (xs @ ys)
[PROOF STEP]
unfolding af\<^sub>G_F Or_prop_entailment
[PROOF STATE]
proof (prove)
using this:
af\<^sub>G \<phi> ys \<in> set (map (af\<^sub>G \<phi>) (suffixes (xs @ ys)))

goal (1 subgoal):
 1. Bex (set (F \<phi> # map (af\<^sub>G \<phi>) (suffixes (xs @ ys)))) ((\<Turnstile>\<^sub>P) S)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
af\<^sub>G \<phi> ys \<in> set (map (af\<^sub>G \<phi>) (suffixes (xs @ ys)))
S \<Turnstile>\<^sub>P af\<^sub>G \<phi> ys

goal (1 subgoal):
 1. Bex (set (F \<phi> # map (af\<^sub>G \<phi>) (suffixes (xs @ ys)))) ((\<Turnstile>\<^sub>P) S)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
S \<Turnstile>\<^sub>P af\<^sub>G (F \<phi>) (xs @ ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma G_af_simp[simp]:
  "\<^bold>G (af \<phi> w) = \<^bold>G \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>G (af \<phi> w) = \<^bold>G \<phi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<^bold>G (af \<phi> w) = \<^bold>G \<phi>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<^bold>G (af \<phi> w) = \<^bold>G \<phi>
[PROOF STEP]
fix \<phi> \<nu>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<^bold>G (af \<phi> w) = \<^bold>G \<phi>
[PROOF STEP]
have "\<^bold>G (af_letter \<phi> \<nu>) = \<^bold>G \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>G (af_letter \<phi> \<nu>) = \<^bold>G \<phi>
[PROOF STEP]
by (induction \<phi>) auto
[PROOF STATE]
proof (state)
this:
\<^bold>G (af_letter \<phi> \<nu>) = \<^bold>G \<phi>

goal (1 subgoal):
 1. \<^bold>G (af \<phi> w) = \<^bold>G \<phi>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<^bold>G (af_letter ?\<phi>'2 ?\<nu>2) = \<^bold>G ?\<phi>'2

goal (1 subgoal):
 1. \<^bold>G (af \<phi> w) = \<^bold>G \<phi>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bold>G (af_letter ?\<phi>'2 ?\<nu>2) = \<^bold>G ?\<phi>'2

goal (1 subgoal):
 1. \<^bold>G (af \<phi> w) = \<^bold>G \<phi>
[PROOF STEP]
by (induction w arbitrary: \<phi> rule: rev_induct) fastforce+
[PROOF STATE]
proof (state)
this:
\<^bold>G (af \<phi> w) = \<^bold>G \<phi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma G_af\<^sub>G_simp[simp]:
  "\<^bold>G (af\<^sub>G \<phi> w) = \<^bold>G \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>G (af\<^sub>G \<phi> w) = \<^bold>G \<phi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<^bold>G (af\<^sub>G \<phi> w) = \<^bold>G \<phi>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<^bold>G (af\<^sub>G \<phi> w) = \<^bold>G \<phi>
[PROOF STEP]
fix \<phi> \<nu>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<^bold>G (af\<^sub>G \<phi> w) = \<^bold>G \<phi>
[PROOF STEP]
have "\<^bold>G (af_G_letter \<phi> \<nu>) = \<^bold>G \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>G (af_G_letter \<phi> \<nu>) = \<^bold>G \<phi>
[PROOF STEP]
by (induction \<phi>) auto
[PROOF STATE]
proof (state)
this:
\<^bold>G (af_G_letter \<phi> \<nu>) = \<^bold>G \<phi>

goal (1 subgoal):
 1. \<^bold>G (af\<^sub>G \<phi> w) = \<^bold>G \<phi>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<^bold>G (af_G_letter ?\<phi>'2 ?\<nu>2) = \<^bold>G ?\<phi>'2

goal (1 subgoal):
 1. \<^bold>G (af\<^sub>G \<phi> w) = \<^bold>G \<phi>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bold>G (af_G_letter ?\<phi>'2 ?\<nu>2) = \<^bold>G ?\<phi>'2

goal (1 subgoal):
 1. \<^bold>G (af\<^sub>G \<phi> w) = \<^bold>G \<phi>
[PROOF STEP]
by (induction w arbitrary: \<phi> rule: rev_induct) fastforce+
[PROOF STATE]
proof (state)
this:
\<^bold>G (af\<^sub>G \<phi> w) = \<^bold>G \<phi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma af_G_letter_free_F:
  "\<^bold>G \<phi> = {} \<Longrightarrow> \<^bold>G (af_letter \<phi> \<nu>) = {}"
  "\<^bold>G \<phi> = {} \<Longrightarrow> \<^bold>G (af_G_letter \<phi> \<nu>) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<^bold>G \<phi> = {} \<Longrightarrow> \<^bold>G (af_letter \<phi> \<nu>) = {}) &&& (\<^bold>G \<phi> = {} \<Longrightarrow> \<^bold>G (af_G_letter \<phi> \<nu>) = {})
[PROOF STEP]
by (induction \<phi>) auto


[STATEMENT]
lemma af_G_free:
  assumes "\<^bold>G \<phi> = {}"
  shows "af \<phi> w = af\<^sub>G \<phi> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af \<phi> w = af\<^sub>G \<phi> w
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<^bold>G \<phi> = {}

goal (1 subgoal):
 1. af \<phi> w = af\<^sub>G \<phi> w
[PROOF STEP]
proof (induction w arbitrary: \<phi>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi>. \<^bold>G \<phi> = {} \<Longrightarrow> af \<phi> [] = af\<^sub>G \<phi> []
 2. \<And>a w \<phi>. \<lbrakk>\<And>\<phi>. \<^bold>G \<phi> = {} \<Longrightarrow> af \<phi> w = af\<^sub>G \<phi> w; \<^bold>G \<phi> = {}\<rbrakk> \<Longrightarrow> af \<phi> (a # w) = af\<^sub>G \<phi> (a # w)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<^bold>G ?\<phi> = {} \<Longrightarrow> af ?\<phi> xs = af\<^sub>G ?\<phi> xs
\<^bold>G \<phi> = {}

goal (2 subgoals):
 1. \<And>\<phi>. \<^bold>G \<phi> = {} \<Longrightarrow> af \<phi> [] = af\<^sub>G \<phi> []
 2. \<And>a w \<phi>. \<lbrakk>\<And>\<phi>. \<^bold>G \<phi> = {} \<Longrightarrow> af \<phi> w = af\<^sub>G \<phi> w; \<^bold>G \<phi> = {}\<rbrakk> \<Longrightarrow> af \<phi> (a # w) = af\<^sub>G \<phi> (a # w)
[PROOF STEP]
hence "af (af_letter \<phi> x) xs = af\<^sub>G (af_letter \<phi> x) xs"
[PROOF STATE]
proof (prove)
using this:
\<^bold>G ?\<phi> = {} \<Longrightarrow> af ?\<phi> xs = af\<^sub>G ?\<phi> xs
\<^bold>G \<phi> = {}

goal (1 subgoal):
 1. af (af_letter \<phi> x) xs = af\<^sub>G (af_letter \<phi> x) xs
[PROOF STEP]
using af_G_letter_free_F[OF Cons.prems, THEN Cons.IH]
[PROOF STATE]
proof (prove)
using this:
\<^bold>G ?\<phi> = {} \<Longrightarrow> af ?\<phi> xs = af\<^sub>G ?\<phi> xs
\<^bold>G \<phi> = {}
af (af_letter \<phi> ?\<nu>1) xs = af\<^sub>G (af_letter \<phi> ?\<nu>1) xs
af (af_G_letter \<phi> ?\<nu>1) xs = af\<^sub>G (af_G_letter \<phi> ?\<nu>1) xs

goal (1 subgoal):
 1. af (af_letter \<phi> x) xs = af\<^sub>G (af_letter \<phi> x) xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
af (af_letter \<phi> x) xs = af\<^sub>G (af_letter \<phi> x) xs

goal (2 subgoals):
 1. \<And>\<phi>. \<^bold>G \<phi> = {} \<Longrightarrow> af \<phi> [] = af\<^sub>G \<phi> []
 2. \<And>a w \<phi>. \<lbrakk>\<And>\<phi>. \<^bold>G \<phi> = {} \<Longrightarrow> af \<phi> w = af\<^sub>G \<phi> w; \<^bold>G \<phi> = {}\<rbrakk> \<Longrightarrow> af \<phi> (a # w) = af\<^sub>G \<phi> (a # w)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
af (af_letter \<phi> x) xs = af\<^sub>G (af_letter \<phi> x) xs

goal (2 subgoals):
 1. \<And>\<phi>. \<^bold>G \<phi> = {} \<Longrightarrow> af \<phi> [] = af\<^sub>G \<phi> []
 2. \<And>a w \<phi>. \<lbrakk>\<And>\<phi>. \<^bold>G \<phi> = {} \<Longrightarrow> af \<phi> w = af\<^sub>G \<phi> w; \<^bold>G \<phi> = {}\<rbrakk> \<Longrightarrow> af \<phi> (a # w) = af\<^sub>G \<phi> (a # w)
[PROOF STEP]
have "af_letter \<phi> x = af_G_letter \<phi> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. af_letter \<phi> x = af_G_letter \<phi> x
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
\<^bold>G \<phi> = {}

goal (1 subgoal):
 1. af_letter \<phi> x = af_G_letter \<phi> x
[PROOF STEP]
by (induction \<phi>) auto
[PROOF STATE]
proof (state)
this:
af_letter \<phi> x = af_G_letter \<phi> x

goal (2 subgoals):
 1. \<And>\<phi>. \<^bold>G \<phi> = {} \<Longrightarrow> af \<phi> [] = af\<^sub>G \<phi> []
 2. \<And>a w \<phi>. \<lbrakk>\<And>\<phi>. \<^bold>G \<phi> = {} \<Longrightarrow> af \<phi> w = af\<^sub>G \<phi> w; \<^bold>G \<phi> = {}\<rbrakk> \<Longrightarrow> af \<phi> (a # w) = af\<^sub>G \<phi> (a # w)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
af (af_letter \<phi> x) xs = af\<^sub>G (af_letter \<phi> x) xs
af_letter \<phi> x = af_G_letter \<phi> x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
af (af_letter \<phi> x) xs = af\<^sub>G (af_letter \<phi> x) xs
af_letter \<phi> x = af_G_letter \<phi> x

goal (1 subgoal):
 1. af \<phi> (x # xs) = af\<^sub>G \<phi> (x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
af \<phi> (x # xs) = af\<^sub>G \<phi> (x # xs)

goal (1 subgoal):
 1. \<And>\<phi>. \<^bold>G \<phi> = {} \<Longrightarrow> af \<phi> [] = af\<^sub>G \<phi> []
[PROOF STEP]
qed simp


[STATEMENT]
lemma af_equals_af\<^sub>G_base_cases:
  "af true w = af\<^sub>G true w"
  "af false w = af\<^sub>G false w"
  "af p(a) w = af\<^sub>G p(a) w"
  "af (np(a)) w = af\<^sub>G (np(a)) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (af true w = af\<^sub>G true w &&& af false w = af\<^sub>G false w) &&& af p(a) w = af\<^sub>G p(a) w &&& af (np(a)) w = af\<^sub>G (np(a)) w
[PROOF STEP]
by (auto intro: af_G_free)