[STATEMENT]
theorem card_farey_fractions_asymptotics'':
  "(\<lambda>N. real (card (farey_fractions N))) \<sim>[at_top] (\<lambda>N. 3 / pi\<^sup>2 * (real N)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>N. real (card (farey_fractions N))) \<sim>[sequentially] (\<lambda>N. 3 / pi\<^sup>2 * (real N)\<^sup>2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>N. real (card (farey_fractions N))) \<sim>[sequentially] (\<lambda>N. 3 / pi\<^sup>2 * (real N)\<^sup>2)
[PROOF STEP]
have "(\<lambda>N. real (card (farey_fractions N)) - 3 / pi\<^sup>2 * (real N) ^ 2) \<in> O(\<lambda>N. real N * ln (real N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>N. real (card (farey_fractions N)) - 3 / pi\<^sup>2 * (real N)\<^sup>2) \<in> O(\<lambda>N. real N * ln (real N))
[PROOF STEP]
by (rule card_farey_fractions_asymptotics)
[PROOF STATE]
proof (state)
this:
(\<lambda>N. real (card (farey_fractions N)) - 3 / pi\<^sup>2 * (real N)\<^sup>2) \<in> O(\<lambda>N. real N * ln (real N))

goal (1 subgoal):
 1. (\<lambda>N. real (card (farey_fractions N))) \<sim>[sequentially] (\<lambda>N. 3 / pi\<^sup>2 * (real N)\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>N. real (card (farey_fractions N)) - 3 / pi\<^sup>2 * (real N)\<^sup>2) \<in> O(\<lambda>N. real N * ln (real N))

goal (1 subgoal):
 1. (\<lambda>N. real (card (farey_fractions N))) \<sim>[sequentially] (\<lambda>N. 3 / pi\<^sup>2 * (real N)\<^sup>2)
[PROOF STEP]
have "(\<lambda>N. real N * ln (real N)) \<in> o(\<lambda>N. 3 / pi ^ 2 * real N ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>N. real N * ln (real N)) \<in> o(\<lambda>N. 3 / pi\<^sup>2 * (real N)\<^sup>2)
[PROOF STEP]
by (rule landau_o.small.compose[OF _ filterlim_real_sequentially]) simp
[PROOF STATE]
proof (state)
this:
(\<lambda>N. real N * ln (real N)) \<in> o(\<lambda>N. 3 / pi\<^sup>2 * (real N)\<^sup>2)

goal (1 subgoal):
 1. (\<lambda>N. real (card (farey_fractions N))) \<sim>[sequentially] (\<lambda>N. 3 / pi\<^sup>2 * (real N)\<^sup>2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>N. real (card (farey_fractions N)) - 3 / pi\<^sup>2 * (real N)\<^sup>2) \<in> o(\<lambda>N. 3 / pi\<^sup>2 * (real N)\<^sup>2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>N. real (card (farey_fractions N)) - 3 / pi\<^sup>2 * (real N)\<^sup>2) \<in> o(\<lambda>N. 3 / pi\<^sup>2 * (real N)\<^sup>2)

goal (1 subgoal):
 1. (\<lambda>N. real (card (farey_fractions N))) \<sim>[sequentially] (\<lambda>N. 3 / pi\<^sup>2 * (real N)\<^sup>2)
[PROOF STEP]
by (simp add: asymp_equiv_altdef)
[PROOF STATE]
proof (state)
this:
(\<lambda>N. real (card (farey_fractions N))) \<sim>[sequentially] (\<lambda>N. 3 / pi\<^sup>2 * (real N)\<^sup>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem two_posts_secure:
  "secure"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. secure
[PROOF STEP]
using Post1.secure Post2.secure
[PROOF STATE]
proof (prove)
using this:
Post1.secure
Post2.secure

goal (1 subgoal):
 1. secure
[PROOF STEP]
by (rule two_secure)


[STATEMENT]
lemma selectlike_compose [simp]: "selectlike (selectlike X \<nu> V) \<nu> W = selectlike X \<nu> (V\<union>W)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. selectlike (selectlike X \<nu> V) \<nu> W = selectlike X \<nu> (V \<union> W)
[PROOF STEP]
by (auto simp add: selectlike_def)


[STATEMENT]
lemma l2_obs_iagreement_Init [iff]: "oreach l2 \<subseteq> l2_iagreement_Init"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oreach l2 \<subseteq> l2_iagreement_Init
[PROOF STEP]
apply (rule external_invariant_translation
         [OF l1_obs_iagreement_Init _ l2_implements_l1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. med12s -` l2_iagreement_Init \<subseteq> l2_iagreement_Init
[PROOF STEP]
apply (auto simp add: med12s_def l1_iagreement_Init_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gen_wf_invar_trans: "rel_fun cr_gen_cfg_wf (=) gen_wf_invar gen_wf_invar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun cr_gen_cfg_wf (=) (\<lambda>_. True) (\<lambda>_. True)
[PROOF STEP]
by auto


[STATEMENT]
lemma rt_fresher_trans_rt_strictly_fresher [elim, trans]:
  assumes "rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2"
      and "rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3"
    shows "rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
from \<open>rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2\<close>
[PROOF STATE]
proof (chain)
picking this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2
[PROOF STEP]
have "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2"
                           and "\<not>(rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1)"
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 &&& \<not> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
unfolding rt_strictly_fresher_def''
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 \<and> \<not> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2 &&& \<not> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
\<not> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
from this(1) and \<open>rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3\<close>
[PROOF STATE]
proof (chain)
picking this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
have "rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3"
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt2
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
from \<open>\<not>(rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
have "\<not>(rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1)"
[PROOF STATE]
proof (prove)
using this:
\<not> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. \<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
proof (rule contrapos_nn)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1 \<Longrightarrow> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
assume "rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1"
[PROOF STATE]
proof (state)
this:
rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1 \<Longrightarrow> rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
with \<open>rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3\<close>
[PROOF STATE]
proof (chain)
picking this:
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
show "rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1"
[PROOF STATE]
proof (prove)
using this:
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rt2 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
show "rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3"
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3
[PROOF STEP]
unfolding rt_strictly_fresher_def''
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3
\<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1

goal (1 subgoal):
 1. rt1 \<sqsubseteq>\<^bsub>dip\<^esub> rt3 \<and> \<not> rt3 \<sqsubseteq>\<^bsub>dip\<^esub> rt1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rt1 \<sqsubset>\<^bsub>dip\<^esub> rt3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma keys_hom_component: "keys (hom_component p n) = {t. t \<in> keys p \<and> deg_pm t = n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (hom_component p n) = {t \<in> keys p. deg_pm t = n}
[PROOF STEP]
by (auto simp: hom_component_def keys_except)


[STATEMENT]
lemma restrict_indets_dehomogenize [simp]: "restrict_indets (dehomogenize None p) = restrict_indets p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict_indets (dehomogenize None p) = restrict_indets p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. restrict_indets (dehomogenize None p) = restrict_indets p
[PROOF STEP]
have eq: "poly_subst (\<lambda>x. (monomial 1 (restrict_indets_subst x))) (dehomo_subst None y) =
            monomial 1 (restrict_indets_subst y)" for y::"'x option"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_subst (\<lambda>x. monomial (1::'c) (restrict_indets_subst x)) (dehomo_subst None y) = monomial (1::'c) (restrict_indets_subst y)
[PROOF STEP]
by (auto simp: restrict_indets_subst_def dehomo_subst_def poly_subst_monomial subst_pp_single)
[PROOF STATE]
proof (state)
this:
poly_subst (\<lambda>x. monomial (1::?'c2) (restrict_indets_subst x)) (dehomo_subst None ?y1) = monomial (1::?'c2) (restrict_indets_subst ?y1)

goal (1 subgoal):
 1. restrict_indets (dehomogenize None p) = restrict_indets p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict_indets (dehomogenize None p) = restrict_indets p
[PROOF STEP]
by (simp only: dehomogenize_def restrict_indets_def poly_subst_poly_subst eq)
[PROOF STATE]
proof (state)
this:
restrict_indets (dehomogenize None p) = restrict_indets p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma focus_in_Polys':
  assumes "p \<in> P[Y]"
  shows "focus X p \<in> P[Y \<inter> X]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. focus X p \<in> P[Y \<inter> X]
[PROOF STEP]
proof (intro PolysI subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> keys (focus X p) \<Longrightarrow> x \<in> .[Y \<inter> X]
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> keys (focus X p) \<Longrightarrow> x \<in> .[Y \<inter> X]
[PROOF STEP]
assume "t \<in> keys (focus X p)"
[PROOF STATE]
proof (state)
this:
t \<in> keys (focus X p)

goal (1 subgoal):
 1. \<And>x. x \<in> keys (focus X p) \<Longrightarrow> x \<in> .[Y \<inter> X]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> keys (focus X p)
[PROOF STEP]
obtain s where "s \<in> keys p" and t: "t = except s (- X)"
[PROOF STATE]
proof (prove)
using this:
t \<in> keys (focus X p)

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> keys p; t = except s (- X)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding keys_focus
[PROOF STATE]
proof (prove)
using this:
t \<in> (\<lambda>t. except t (- X)) ` keys p

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> keys p; t = except s (- X)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
s \<in> keys p
t = except s (- X)

goal (1 subgoal):
 1. \<And>x. x \<in> keys (focus X p) \<Longrightarrow> x \<in> .[Y \<inter> X]
[PROOF STEP]
note this(1)
[PROOF STATE]
proof (state)
this:
s \<in> keys p

goal (1 subgoal):
 1. \<And>x. x \<in> keys (focus X p) \<Longrightarrow> x \<in> .[Y \<inter> X]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
s \<in> keys p

goal (1 subgoal):
 1. \<And>x. x \<in> keys (focus X p) \<Longrightarrow> x \<in> .[Y \<inter> X]
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
p \<in> P[Y]
[PROOF STEP]
have "keys p \<subseteq> .[Y]"
[PROOF STATE]
proof (prove)
using this:
p \<in> P[Y]

goal (1 subgoal):
 1. keys p \<subseteq> .[Y]
[PROOF STEP]
by (rule PolysD)
[PROOF STATE]
proof (state)
this:
keys p \<subseteq> .[Y]

goal (1 subgoal):
 1. \<And>x. x \<in> keys (focus X p) \<Longrightarrow> x \<in> .[Y \<inter> X]
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
s \<in> .[Y]
[PROOF STEP]
have "keys s \<subseteq> Y"
[PROOF STATE]
proof (prove)
using this:
s \<in> .[Y]

goal (1 subgoal):
 1. keys s \<subseteq> Y
[PROOF STEP]
by (rule PPsD)
[PROOF STATE]
proof (state)
this:
keys s \<subseteq> Y

goal (1 subgoal):
 1. \<And>x. x \<in> keys (focus X p) \<Longrightarrow> x \<in> .[Y \<inter> X]
[PROOF STEP]
hence "keys t \<subseteq> Y \<inter> X"
[PROOF STATE]
proof (prove)
using this:
keys s \<subseteq> Y

goal (1 subgoal):
 1. keys t \<subseteq> Y \<inter> X
[PROOF STEP]
by (simp add: t keys_except le_infI1)
[PROOF STATE]
proof (state)
this:
keys t \<subseteq> Y \<inter> X

goal (1 subgoal):
 1. \<And>x. x \<in> keys (focus X p) \<Longrightarrow> x \<in> .[Y \<inter> X]
[PROOF STEP]
thus "t \<in> .[Y \<inter> X]"
[PROOF STATE]
proof (prove)
using this:
keys t \<subseteq> Y \<inter> X

goal (1 subgoal):
 1. t \<in> .[Y \<inter> X]
[PROOF STEP]
by (rule PPsI)
[PROOF STATE]
proof (state)
this:
t \<in> .[Y \<inter> X]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lst_head_cons_pair:
  fixes y1::"'a ::at" and y2::"'a::at" and x1::"'b::fs" and x2::"'b::fs" and xs1::"('b::fs) list" and xs2::"('b::fs) list"
  assumes "[[atom y1]]lst. (x1 # xs1) = [[atom y2]]lst. (x2 # xs2)"
  shows "[[atom y1]]lst. (x1,xs1) = [[atom y2]]lst. (x2,xs2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[atom y1]]lst. (x1, xs1) = [[atom y2]]lst. (x2, xs2)
[PROOF STEP]
proof(subst  Abs1_eq_iff_all(3)[of y1 "(x1,xs1)"  y2 "(x2,xs2)"],rule,rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>atom c \<sharp> ?z; atom c \<sharp> (y1, y2, (x1, xs1), x2, xs2)\<rbrakk> \<Longrightarrow> (y1 \<leftrightarrow> c) \<bullet> (x1, xs1) = (y2 \<leftrightarrow> c) \<bullet> (x2, xs2)
[PROOF STEP]
fix c::'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>atom c \<sharp> ?z; atom c \<sharp> (y1, y2, (x1, xs1), x2, xs2)\<rbrakk> \<Longrightarrow> (y1 \<leftrightarrow> c) \<bullet> (x1, xs1) = (y2 \<leftrightarrow> c) \<bullet> (x2, xs2)
[PROOF STEP]
assume "atom c \<sharp> (x1#xs1,x2#xs2)" and "atom c \<sharp> (y1, y2, (x1, xs1), x2, xs2)"
[PROOF STATE]
proof (state)
this:
atom c \<sharp> (x1 # xs1, x2 # xs2)
atom c \<sharp> (y1, y2, (x1, xs1), x2, xs2)

goal (1 subgoal):
 1. \<And>c. \<lbrakk>atom c \<sharp> ?z; atom c \<sharp> (y1, y2, (x1, xs1), x2, xs2)\<rbrakk> \<Longrightarrow> (y1 \<leftrightarrow> c) \<bullet> (x1, xs1) = (y2 \<leftrightarrow> c) \<bullet> (x2, xs2)
[PROOF STEP]
thus  "(y1 \<leftrightarrow> c) \<bullet> (x1, xs1) = (y2 \<leftrightarrow> c) \<bullet> (x2, xs2)"
[PROOF STATE]
proof (prove)
using this:
atom c \<sharp> (x1 # xs1, x2 # xs2)
atom c \<sharp> (y1, y2, (x1, xs1), x2, xs2)

goal (1 subgoal):
 1. (y1 \<leftrightarrow> c) \<bullet> (x1, xs1) = (y2 \<leftrightarrow> c) \<bullet> (x2, xs2)
[PROOF STEP]
using assms Abs1_eq_iff_all(3)
[PROOF STATE]
proof (prove)
using this:
atom c \<sharp> (x1 # xs1, x2 # xs2)
atom c \<sharp> (y1, y2, (x1, xs1), x2, xs2)
[[atom y1]]lst. x1 # xs1 = [[atom y2]]lst. x2 # xs2
([[atom ?a]]lst. ?x = [[atom ?b]]lst. ?y) = (\<forall>c. atom c \<sharp> ?z \<longrightarrow> atom c \<sharp> (?a, ?b, ?x, ?y) \<longrightarrow> (?a \<leftrightarrow> c) \<bullet> ?x = (?b \<leftrightarrow> c) \<bullet> ?y)

goal (1 subgoal):
 1. (y1 \<leftrightarrow> c) \<bullet> (x1, xs1) = (y2 \<leftrightarrow> c) \<bullet> (x2, xs2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(y1 \<leftrightarrow> c) \<bullet> (x1, xs1) = (y2 \<leftrightarrow> c) \<bullet> (x2, xs2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem completeness_countable:
  assumes inf_uni: "infinite (UNIV :: ('u :: countable) set)"
  assumes finite_cs: "finite Cs" "\<forall>C\<in>Cs. finite C"
  assumes unsat: "\<forall>(F::'u fun_denot) (G::'u pred_denot). \<not>eval\<^sub>c\<^sub>s F G Cs"
  shows "\<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'
[PROOF STEP]
have "\<forall>(F::hterm fun_denot) (G::hterm pred_denot) . \<not>eval\<^sub>c\<^sub>s F G Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>F G. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
proof (rule; rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F G. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
fix F :: "hterm fun_denot"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F G. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
fix G :: "hterm pred_denot"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F G. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
obtain u_of_hterm :: "hterm \<Rightarrow> 'u" where p_u_of_hterm: "bij u_of_hterm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u_of_hterm. bij u_of_hterm \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using countably_inf_bij inf_uni infinite_hterms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>infinite UNIV; infinite UNIV\<rbrakk> \<Longrightarrow> \<exists>b_of_a. bij b_of_a
infinite UNIV
infinite UNIV

goal (1 subgoal):
 1. (\<And>u_of_hterm. bij u_of_hterm \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij u_of_hterm

goal (1 subgoal):
 1. \<And>F G. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
let ?F = "F_conv u_of_hterm F"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F G. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
let ?G = "G_conv u_of_hterm G"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F G. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
have "\<not> eval\<^sub>c\<^sub>s ?F ?G Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s (F_conv u_of_hterm F) (G_conv u_of_hterm G) Cs
[PROOF STEP]
using unsat
[PROOF STATE]
proof (prove)
using this:
\<forall>F G. \<not> eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s (F_conv u_of_hterm F) (G_conv u_of_hterm G) Cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> eval\<^sub>c\<^sub>s (F_conv u_of_hterm F) (G_conv u_of_hterm G) Cs

goal (1 subgoal):
 1. \<And>F G. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> eval\<^sub>c\<^sub>s (F_conv u_of_hterm F) (G_conv u_of_hterm G) Cs
[PROOF STEP]
show "\<not> eval\<^sub>c\<^sub>s F G Cs"
[PROOF STATE]
proof (prove)
using this:
\<not> eval\<^sub>c\<^sub>s (F_conv u_of_hterm F) (G_conv u_of_hterm G) Cs

goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
using eval\<^sub>c\<^sub>s_bij
[PROOF STATE]
proof (prove)
using this:
\<not> eval\<^sub>c\<^sub>s (F_conv u_of_hterm F) (G_conv u_of_hterm G) Cs
bij ?b_of_a \<Longrightarrow> eval\<^sub>c\<^sub>s (F_conv ?b_of_a ?F) (G_conv ?b_of_a ?G) ?Cs = eval\<^sub>c\<^sub>s ?F ?G ?Cs

goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
using p_u_of_hterm
[PROOF STATE]
proof (prove)
using this:
\<not> eval\<^sub>c\<^sub>s (F_conv u_of_hterm F) (G_conv u_of_hterm G) Cs
bij ?b_of_a \<Longrightarrow> eval\<^sub>c\<^sub>s (F_conv ?b_of_a ?F) (G_conv ?b_of_a ?G) ?Cs = eval\<^sub>c\<^sub>s ?F ?G ?Cs
bij u_of_hterm

goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> eval\<^sub>c\<^sub>s F G Cs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>F G. \<not> eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. \<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>F G. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
show "\<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'"
[PROOF STATE]
proof (prove)
using this:
\<forall>F G. \<not> eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. \<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'
[PROOF STEP]
using finite_cs completeness
[PROOF STATE]
proof (prove)
using this:
\<forall>F G. \<not> eval\<^sub>c\<^sub>s F G Cs
finite Cs
\<forall>C\<in>Cs. finite C
\<lbrakk>finite ?Cs; \<forall>C\<in>?Cs. finite C; \<forall>F G. \<not> eval\<^sub>c\<^sub>s F G ?Cs\<rbrakk> \<Longrightarrow> \<exists>Cs'. resolution_deriv ?Cs Cs' \<and> {} \<in> Cs'

goal (1 subgoal):
 1. \<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma imp_igSwapBinpIPresIGWlsBinpSTR:
"igSwapAbsIPresIGWlsAbsSTR MOD \<Longrightarrow> igSwapBinpIPresIGWlsBinpSTR MOD"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igSwapAbsIPresIGWlsAbsSTR MOD \<Longrightarrow> igSwapBinpIPresIGWlsBinpSTR MOD
[PROOF STEP]
by (simp add:
igSwapBinpIPresIGWlsBinpSTR_def igSwapAbsIPresIGWlsAbsSTR_def igSwapBinp_def
igWlsBinp_def liftAll2_def lift_def sameDom_def
split: option.splits) (smt option.distinct(1) option.exhaust surj_pair)


[STATEMENT]
lemma comp_ipresIGAbs:
assumes "ipresIGWls h MOD MOD'"
and "ipresIGAbs h hA MOD MOD'" and "ipresIGAbs h' hA' MOD' MOD''"
shows "ipresIGAbs (h' o h) (hA' o hA) MOD MOD''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipresIGAbs (h' \<circ> h) (hA' \<circ> hA) MOD MOD''
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ipresIGWls h MOD MOD'
ipresIGAbs h hA MOD MOD'
ipresIGAbs h' hA' MOD' MOD''

goal (1 subgoal):
 1. ipresIGAbs (h' \<circ> h) (hA' \<circ> hA) MOD MOD''
[PROOF STEP]
unfolding ipresIGWls_def ipresIGAbs_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s X. igWls MOD s X \<longrightarrow> igWls MOD' s (h X)
\<forall>xs x s X. isInBar (xs, s) \<and> igWls MOD s X \<longrightarrow> hA (igAbs MOD xs x X) = igAbs MOD' xs x (h X)
\<forall>xs x s X. isInBar (xs, s) \<and> igWls MOD' s X \<longrightarrow> hA' (igAbs MOD' xs x X) = igAbs MOD'' xs x (h' X)

goal (1 subgoal):
 1. \<forall>xs x s X. isInBar (xs, s) \<and> igWls MOD s X \<longrightarrow> (hA' \<circ> hA) (igAbs MOD xs x X) = igAbs MOD'' xs x ((h' \<circ> h) X)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma fm_member_split: \<open>k |\<in>| fmdom N' \<Longrightarrow> \<exists>N'' v. N' = fmupd k v N'' \<and> the (fmlookup N' k) = v \<and>
    k |\<notin>| fmdom N''\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k |\<in>| fmdom N' \<Longrightarrow> \<exists>N'' v. N' = fmupd k v N'' \<and> the (fmlookup N' k) = v \<and> k |\<notin>| fmdom N''
[PROOF STEP]
by (rule exI[of _ \<open>fmdrop k N'\<close>])
    (auto simp: fmupd_fmdrop_id)


[STATEMENT]
lemma \<open>fmdrop k (fmupd k va N'') = fmdrop k N''\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmdrop k (fmupd k va N'') = fmdrop k N''
[PROOF STEP]
by (simp add: fmap_ext)


[STATEMENT]
lemma prove_last_completeness:
  assumes "a' \<succeq> a"
      and "Some a = nf1 \<oplus> f2"
    shows "a' \<ominus> nf1 \<succeq> f2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a' \<ominus> nf1 \<succeq> f2
[PROOF STEP]
by (meson assms(1) assms(2) greater_def greater_minus_trans minus_bigger succ_trans)


[STATEMENT]
lemma Arr_in_mkarr:
    assumes "Arr t"
    shows "t \<in> mkarr t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> mkarr t
[PROOF STEP]
using assms mkarr_def
[PROOF STATE]
proof (prove)
using this:
Arr t
mkarr ?t = {u. local.equiv ?t u}

goal (1 subgoal):
 1. t \<in> mkarr t
[PROOF STEP]
by simp


[STATEMENT]
lemma tsp__nosp:
  assumes "A B C TSP P Q"
  shows "\<not> A B C OSP P Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> A B C OSP P Q
[PROOF STEP]
using assms l9_41_2 tsp_distincts
[PROOF STATE]
proof (prove)
using this:
A B CTSP P Q
\<lbrakk>?A ?B ?CTSP ?P ?R; ?A ?B ?C OSP ?P ?Q\<rbrakk> \<Longrightarrow> ?A ?B ?CTSP ?Q ?R
?A ?B ?CTSP ?P ?Q \<Longrightarrow> ?A \<noteq> ?B \<and> ?A \<noteq> ?C \<and> ?B \<noteq> ?C \<and> ?A \<noteq> ?P \<and> ?B \<noteq> ?P \<and> ?C \<noteq> ?P \<and> ?A \<noteq> ?Q \<and> ?B \<noteq> ?Q \<and> ?C \<noteq> ?Q \<and> ?P \<noteq> ?Q

goal (1 subgoal):
 1. \<not> A B C OSP P Q
[PROOF STEP]
by blast


[STATEMENT]
lemma ncol_conga_ncol:
  assumes "\<not> Col A B C" and
    "A B C CongA D E F"
  shows "\<not> Col D E F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Col D E F
[PROOF STEP]
using assms(1) assms(2) col_conga_col conga_sym
[PROOF STATE]
proof (prove)
using this:
\<not> Col A B C
A B C CongA D E F
\<lbrakk>Col ?A ?B ?C; ?A ?B ?C CongA ?D ?E ?F\<rbrakk> \<Longrightarrow> Col ?D ?E ?F
?A ?B ?C CongA ?A' ?B' ?C' \<Longrightarrow> ?A' ?B' ?C' CongA ?A ?B ?C

goal (1 subgoal):
 1. \<not> Col D E F
[PROOF STEP]
by blast


[STATEMENT]
lemma conga_sams_nos__nts:
  assumes "SAMS A B C D E F" and
    "C B J CongA D E F" and
    "\<not> B C OS A J"
  shows "\<not> A B TS C J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> A B TS C J
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> A B TS C J
[PROOF STEP]
have "SAMS A B C C B J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAMS A B C C B J
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. SAMS A B C C B J
[PROOF STEP]
have "A B C CongA A B C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A B C CongA A B C
[PROOF STEP]
using assms(1) conga_refl sams_distincts
[PROOF STATE]
proof (prove)
using this:
SAMS A B C D E F
\<lbrakk>?A \<noteq> ?B; ?C \<noteq> ?B\<rbrakk> \<Longrightarrow> ?A ?B ?C CongA ?A ?B ?C
SAMS ?A ?B ?C ?D ?E ?F \<Longrightarrow> ?A \<noteq> ?B \<and> ?B \<noteq> ?C \<and> ?D \<noteq> ?E \<and> ?E \<noteq> ?F

goal (1 subgoal):
 1. A B C CongA A B C
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
A B C CongA A B C

goal (1 subgoal):
 1. SAMS A B C C B J
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A B C CongA A B C

goal (1 subgoal):
 1. SAMS A B C C B J
[PROOF STEP]
have "D E F CongA C B J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D E F CongA C B J
[PROOF STEP]
using assms(2) not_conga_sym
[PROOF STATE]
proof (prove)
using this:
C B J CongA D E F
\<not> ?A ?B ?C CongA ?D ?E ?F \<Longrightarrow> \<not> ?D ?E ?F CongA ?A ?B ?C

goal (1 subgoal):
 1. D E F CongA C B J
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
D E F CongA C B J

goal (1 subgoal):
 1. SAMS A B C C B J
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A B C CongA A B C
D E F CongA C B J
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A B C CongA A B C
D E F CongA C B J

goal (1 subgoal):
 1. SAMS A B C C B J
[PROOF STEP]
using assms(1) conga2_sams__sams
[PROOF STATE]
proof (prove)
using this:
A B C CongA A B C
D E F CongA C B J
SAMS A B C D E F
\<lbrakk>?A ?B ?C CongA ?A' ?B' ?C'; ?D ?E ?F CongA ?D' ?E' ?F'; SAMS ?A ?B ?C ?D ?E ?F\<rbrakk> \<Longrightarrow> SAMS ?A' ?B' ?C' ?D' ?E' ?F'

goal (1 subgoal):
 1. SAMS A B C C B J
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
SAMS A B C C B J

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
SAMS A B C C B J

goal (1 subgoal):
 1. \<not> A B TS C J
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
SAMS A B C C B J

goal (1 subgoal):
 1. \<not> A B TS C J
[PROOF STEP]
by (simp add: assms(3) sams_nos__nts)
[PROOF STATE]
proof (state)
this:
\<not> A B TS C J

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma con_comp_sinks_range:
 "u \<in> range Some \<Longrightarrow>
  set xs \<subseteq> range p \<union> range q \<Longrightarrow>
    sinks (con_comp_pol I) (con_comp_map D E p q) u xs \<subseteq> range Some"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<in> range Some; set xs \<subseteq> range p \<union> range q\<rbrakk> \<Longrightarrow> sinks (con_comp_pol I) (con_comp_map D E p q) u xs \<subseteq> range Some
[PROOF STEP]
by (insert con_comp_sinks_aux_range [of "{u}" xs p q I D E],
 simp add: sinks_aux_single_dom)


[STATEMENT]
lemma Pbij_inverse_Inverse[rule_format]:
  "\<gamma> = Pbij_inverse \<beta> \<Longrightarrow> (\<forall> l ll . ((l,ll):\<beta>) = ((ll,l):\<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> = Pbij_inverse \<beta> \<Longrightarrow> \<forall>l ll. ((l, ll) \<in> \<beta>) = ((ll, l) \<in> \<gamma>)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> = Pbij_inverse \<beta> \<Longrightarrow> \<forall>l ll. ((l, ll) \<in> \<beta>) = ((ll, l) \<in> \<gamma>)
[PROOF STEP]
by (simp add: Pbij_inverse_def)