[STATEMENT]
lemma eval_Fields'_conv:
  "Predicate.eval (Fields'_i_i_o P C) = Fields' P C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred.eval (Fields'_i_i_o P C) = Fields' P C
[PROOF STEP]
by(auto intro: Fields'_i_i_oI elim: Fields'_i_i_oE intro!: ext)


[STATEMENT]
lemma map_resource_id1: "map_resource id f res = map_resource' f res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_resource id f res = map_resource' f res
[PROOF STEP]
by(coinduction arbitrary: res)(auto simp add: rel_fun_def spmf_rel_map resource.map_sel intro!: rel_spmf_reflI)


[STATEMENT]
lemma ground_PfP [simp]: "ground_fm (PfP y) = ground y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground_fm (PfP y) = ground y
[PROOF STEP]
by (simp add: ground_aux_def ground_fm_aux_def supp_conv_fresh)


[STATEMENT]
lemma is_aligned_iff_dvd_nat:
  \<open>is_aligned ptr n \<longleftrightarrow> 2 ^ n dvd unat ptr\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr n = (2 ^ n dvd unat ptr)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_aligned ptr n = (2 ^ n dvd unat ptr)
[PROOF STEP]
have \<open>unat ptr = nat \<bar>uint ptr\<bar>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat ptr = nat \<bar>uint ptr\<bar>
[PROOF STEP]
by transfer simp
[PROOF STATE]
proof (state)
this:
unat ptr = nat \<bar>uint ptr\<bar>

goal (1 subgoal):
 1. is_aligned ptr n = (2 ^ n dvd unat ptr)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
unat ptr = nat \<bar>uint ptr\<bar>
[PROOF STEP]
have \<open>2 ^ n dvd unat ptr \<longleftrightarrow> 2 ^ n dvd uint ptr\<close>
[PROOF STATE]
proof (prove)
using this:
unat ptr = nat \<bar>uint ptr\<bar>

goal (1 subgoal):
 1. (2 ^ n dvd unat ptr) = (2 ^ n dvd uint ptr)
[PROOF STEP]
by (simp only: dvd_nat_abs_iff) simp
[PROOF STATE]
proof (state)
this:
(2 ^ n dvd unat ptr) = (2 ^ n dvd uint ptr)

goal (1 subgoal):
 1. is_aligned ptr n = (2 ^ n dvd unat ptr)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(2 ^ n dvd unat ptr) = (2 ^ n dvd uint ptr)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(2 ^ n dvd unat ptr) = (2 ^ n dvd uint ptr)

goal (1 subgoal):
 1. is_aligned ptr n = (2 ^ n dvd unat ptr)
[PROOF STEP]
by (simp add: is_aligned_iff_dvd_int)
[PROOF STATE]
proof (state)
this:
is_aligned ptr n = (2 ^ n dvd unat ptr)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aligned_sub_aligned':
  "\<lbrakk> is_aligned (a :: 'a :: len word) n; is_aligned b n; n < LENGTH('a) \<rbrakk>
   \<Longrightarrow> is_aligned (a - b) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned (a - b) n
[PROOF STEP]
by (simp add: aligned_sub_aligned)


[STATEMENT]
lemma cop_stable_no_blocking_on:
  shows "stable_no_blocking_on ds (cop ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_no_blocking_on ds (cop ds)
[PROOF STEP]
proof(rule stable_no_blocking_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (cop ds \<union> X''); X'' \<noteq> Ch h (cop ds); X'' \<subseteq> CD_on ds (cop ds \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix h X''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (cop ds \<union> X''); X'' \<noteq> Ch h (cop ds); X'' \<subseteq> CD_on ds (cop ds \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume C: "X'' = Ch h (CH (fp_cop_F ds) \<union> X'')"
[PROOF STATE]
proof (state)
this:
X'' = Ch h (cop ds \<union> X'')

goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (cop ds \<union> X''); X'' \<noteq> Ch h (cop ds); X'' \<subseteq> CD_on ds (cop ds \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume NE: "X'' \<noteq> Ch h (CH (fp_cop_F ds))"
[PROOF STATE]
proof (state)
this:
X'' \<noteq> Ch h (cop ds)

goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (cop ds \<union> X''); X'' \<noteq> Ch h (cop ds); X'' \<subseteq> CD_on ds (cop ds \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume CD: "X'' \<subseteq> CD_on ds (CH (fp_cop_F ds) \<union> X'')"
[PROOF STATE]
proof (state)
this:
X'' \<subseteq> CD_on ds (cop ds \<union> X'')

goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (cop ds \<union> X''); X'' \<noteq> Ch h (cop ds); X'' \<subseteq> CD_on ds (cop ds \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from CD
[PROOF STATE]
proof (chain)
picking this:
X'' \<subseteq> CD_on ds (cop ds \<union> X'')
[PROOF STEP]
have "X'' \<subseteq> fp_cop_F ds"
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> CD_on ds (cop ds \<union> X'')

goal (1 subgoal):
 1. X'' \<subseteq> fp_cop_F ds
[PROOF STEP]
by (rule X''_closed)
[PROOF STATE]
proof (state)
this:
X'' \<subseteq> fp_cop_F ds

goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (cop ds \<union> X''); X'' \<noteq> Ch h (cop ds); X'' \<subseteq> CD_on ds (cop ds \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X'' \<subseteq> fp_cop_F ds
[PROOF STEP]
have X: "CH (fp_cop_F ds) \<union> X'' \<subseteq> fp_cop_F ds"
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> fp_cop_F ds

goal (1 subgoal):
 1. cop ds \<union> X'' \<subseteq> fp_cop_F ds
[PROOF STEP]
using CH_range
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> fp_cop_F ds
CH ?A \<subseteq> ?A

goal (1 subgoal):
 1. cop ds \<union> X'' \<subseteq> fp_cop_F ds
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cop ds \<union> X'' \<subseteq> fp_cop_F ds

goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (cop ds \<union> X''); X'' \<noteq> Ch h (cop ds); X'' \<subseteq> CD_on ds (cop ds \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from C NE Ch_CH_irc_idem[of h]
[PROOF STATE]
proof (chain)
picking this:
X'' = Ch h (cop ds \<union> X'')
X'' \<noteq> Ch h (cop ds)
Ch h (CH ?A) = Ch h ?A
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
X'' = Ch h (cop ds \<union> X'')
X'' \<noteq> Ch h (cop ds)
Ch h (CH ?A) = Ch h ?A

goal (1 subgoal):
 1. False
[PROOF STEP]
using consistency_onD[OF Ch_consistency _ X] CH_domain Ch_domain
[PROOF STATE]
proof (prove)
using this:
X'' = Ch h (cop ds \<union> X'')
X'' \<noteq> Ch h (cop ds)
Ch h (CH ?A) = Ch h ?A
\<lbrakk>fp_cop_F ds \<subseteq> UNIV; Ch ?h2 (fp_cop_F ds) \<subseteq> cop ds \<union> X''\<rbrakk> \<Longrightarrow> Ch ?h2 (fp_cop_F ds) = Ch ?h2 (cop ds \<union> X'')
CH ?A \<inter> {x. Xh x = ?h} = Ch ?h (?A \<inter> {x. Xh x = ?h})
Ch ?h (?A \<inter> {x. Xh x = ?h}) = Ch ?h ?A

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Cons_le_Cons [iff]: "x#xs [\<sqsubseteq>\<^bsub>r\<^esub>] y#ys = (x \<sqsubseteq>\<^sub>r y \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs [\<sqsubseteq>\<^bsub>r\<^esub>] y # ys) = (x \<sqsubseteq>\<^bsub>r\<^esub> y \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs [\<sqsubseteq>\<^bsub>r\<^esub>] y # ys) = (x \<sqsubseteq>\<^bsub>r\<^esub> y \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys)
[PROOF STEP]
by (simp add: lesub_def Listn.le_def)


[STATEMENT]
lemma Cons_less_Conss [simp]:
  "order r \<Longrightarrow>  x#xs [\<sqsubset>\<^sub>r] y#ys = (x \<sqsubset>\<^sub>r y \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<or> x = y \<and> xs [\<sqsubset>\<^sub>r] ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order r \<Longrightarrow> (x # xs [\<sqsubset>\<^bsub>r\<^esub>] y # ys) = (x \<sqsubset>\<^bsub>r\<^esub> y \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<or> x = y \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order r \<Longrightarrow> (x # xs [\<sqsubset>\<^bsub>r\<^esub>] y # ys) = (x \<sqsubset>\<^bsub>r\<^esub> y \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<or> x = y \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys)
[PROOF STEP]
apply (unfold lesssub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order r \<Longrightarrow> (x # xs [\<sqsubseteq>\<^bsub>r\<^esub>] y # ys \<and> x # xs \<noteq> y # ys) = ((x \<sqsubseteq>\<^bsub>r\<^esub> y \<and> x \<noteq> y) \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<or> x = y \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<and> xs \<noteq> ys)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma isPath_distD: "isPath u p v \<Longrightarrow> dist u (length p) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isPath u p v \<Longrightarrow> dist u (length p) v
[PROOF STEP]
by (auto simp: dist_def)


[STATEMENT]
lemma coeff_of_int_poly [simp]: "coeff (of_int_poly p) n = of_int (coeff p n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff (of_int_poly p) n = of_int (poly.coeff p n)
[PROOF STEP]
by transfer' simp


[STATEMENT]
lemma weak_action_modality_tau:
    "(\<langle>\<langle>\<tau>\<rangle>\<rangle>x) = weak_tau_modality x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>\<langle>\<tau>\<rangle>\<rangle>x = weak_tau_modality x
[PROOF STEP]
unfolding weak_action_modality_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<tau> = \<tau> then weak_tau_modality x else weak_tau_modality (Act \<tau> (weak_tau_modality x))) = weak_tau_modality x
[PROOF STEP]
by simp


[STATEMENT]
lemma (in Universe) UniverseProduct: "Elem u U \<Longrightarrow> Elem (Product u) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Elem u U \<Longrightarrow> Elem (Product u) U
[PROOF STEP]
apply (rule_tac u="(Product u)" and v="Power (CartProd u (Sum u))" in UniverseSubset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Elem u U \<Longrightarrow> HOLZF.subset (Product u) (Power (CartProd u (HOLZF.Sum u)))
 2. Elem u U \<Longrightarrow> Elem (Power (CartProd u (HOLZF.Sum u))) U
[PROOF STEP]
apply (rule ProductSubset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Elem u U \<Longrightarrow> Elem (Power (CartProd u (HOLZF.Sum u))) U
[PROOF STEP]
apply (rule Upow)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Elem u U \<Longrightarrow> Elem (CartProd u (HOLZF.Sum u)) U
[PROOF STEP]
apply (rule UniverseProd, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Elem u U \<Longrightarrow> Elem (HOLZF.Sum u) U
[PROOF STEP]
apply (rule UniverseSum,simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ZFUnionInRangeExplode: "\<lbrakk>A \<in> range explode ; B \<in> range explode\<rbrakk> \<Longrightarrow> A \<union> B \<in> range explode"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> range explode; B \<in> range explode\<rbrakk> \<Longrightarrow> A \<union> B \<in> range explode
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> range explode; B \<in> range explode\<rbrakk> \<Longrightarrow> A \<union> B \<in> range explode
[PROOF STEP]
assume "A \<in> range explode" and "B \<in> range explode"
[PROOF STATE]
proof (state)
this:
A \<in> range explode
B \<in> range explode

goal (1 subgoal):
 1. \<lbrakk>A \<in> range explode; B \<in> range explode\<rbrakk> \<Longrightarrow> A \<union> B \<in> range explode
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
A \<in> range explode
B \<in> range explode
[PROOF STEP]
obtain A' B' where A': "A = explode A'" and B': "B = explode B'"
[PROOF STATE]
proof (prove)
using this:
A \<in> range explode
B \<in> range explode

goal (1 subgoal):
 1. (\<And>A' B'. \<lbrakk>A = explode A'; B = explode B'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = explode A'
B = explode B'

goal (1 subgoal):
 1. \<lbrakk>A \<in> range explode; B \<in> range explode\<rbrakk> \<Longrightarrow> A \<union> B \<in> range explode
[PROOF STEP]
have "A \<union> B = explode (union (implode A) (implode B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<union> B = explode (HOLZF.union (implode A) (implode B))
[PROOF STEP]
by(auto simp add: explode_union  union explode_Elem A' B')
[PROOF STATE]
proof (state)
this:
A \<union> B = explode (HOLZF.union (implode A) (implode B))

goal (1 subgoal):
 1. \<lbrakk>A \<in> range explode; B \<in> range explode\<rbrakk> \<Longrightarrow> A \<union> B \<in> range explode
[PROOF STEP]
thus "A \<union> B \<in> range explode"
[PROOF STATE]
proof (prove)
using this:
A \<union> B = explode (HOLZF.union (implode A) (implode B))

goal (1 subgoal):
 1. A \<union> B \<in> range explode
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<union> B \<in> range explode

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma n_ivl_mono: "(x::ivl) \<sqsubseteq> y \<Longrightarrow> n_ivl x \<le> n_ivl y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubseteq> y \<Longrightarrow> n_ivl x \<le> n_ivl y
[PROOF STEP]
unfolding n_ivl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubseteq> y \<Longrightarrow> 2 - m_ivl x \<le> 2 - m_ivl y
[PROOF STEP]
by (metis diff_le_mono2 m_ivl_anti_mono)


[STATEMENT]
lemma inf_add_K_left: "a \<le>\<^sub>\<K> b + a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b + a
[PROOF STEP]
by (simp only: add_commute, fact inf_add_K_right)


[STATEMENT]
lemma is_regular_add_sheaf_spec:
  assumes "is_regular s U" and "is_regular s' U" and "U \<subseteq> Spec"
  shows "is_regular (add_sheaf_spec U s s') U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_regular (add_sheaf_spec U s s') U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_regular (add_sheaf_spec U s s') U
[PROOF STEP]
have "add_sheaf_spec U s s' \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>" if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U s s' \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_sheaf_spec U s s' \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret pi: pr_ideal R \<pp> "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using \<open>U \<subseteq> Spec\<close>[unfolded spectrum_def] \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
U \<subseteq> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}
\<pp> \<in> U

goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_sheaf_spec U s s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
have "s \<pp> \<in> pi.carrier_local_ring_at"
      "s' \<pp> \<in> pi.carrier_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<pp> \<in> pi.carrier_local_ring_at &&& s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using \<open>is_regular s U\<close> \<open>is_regular s' U\<close>
[PROOF STATE]
proof (prove)
using this:
is_regular s U
is_regular s' U

goal (1 subgoal):
 1. s \<pp> \<in> pi.carrier_local_ring_at &&& s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
unfolding is_regular_def is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))

goal (1 subgoal):
 1. s \<pp> \<in> pi.carrier_local_ring_at &&& s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
\<pp> \<in> U

goal (1 subgoal):
 1. s \<pp> \<in> pi.carrier_local_ring_at &&& s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using assms(3) frac_in_carrier_local
[PROOF STATE]
proof (prove)
using this:
\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
\<pp> \<in> U
U \<subseteq> Spec
\<lbrakk>?\<pp> \<in> Spec; ?r \<in> R; ?s \<in> R; ?s \<notin> ?\<pp>\<rbrakk> \<Longrightarrow> quotient_ring.frac (R\<setminus>?\<pp>) R (+) (\<cdot>) \<zero> ?r ?s \<in> R \<^bsub>?\<pp> (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. s \<pp> \<in> pi.carrier_local_ring_at &&& s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
s \<pp> \<in> pi.carrier_local_ring_at
s' \<pp> \<in> pi.carrier_local_ring_at

goal (1 subgoal):
 1. add_sheaf_spec U s s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<pp> \<in> pi.carrier_local_ring_at
s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<pp> \<in> pi.carrier_local_ring_at
s' \<pp> \<in> pi.carrier_local_ring_at

goal (1 subgoal):
 1. add_sheaf_spec U s s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
unfolding add_sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
s \<pp> \<in> pi.carrier_local_ring_at
s' \<pp> \<in> pi.carrier_local_ring_at

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>) (s' \<pp>)) \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
s \<pp> \<in> pi.carrier_local_ring_at
s' \<pp> \<in> pi.carrier_local_ring_at
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>) (s' \<pp>)) \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
by (simp flip:pi.add_local_ring_at_def)
[PROOF STATE]
proof (state)
this:
add_sheaf_spec U s s' \<pp> \<in> pi.carrier_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> add_sheaf_spec U s s' ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. is_regular (add_sheaf_spec U s s') U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> add_sheaf_spec U s s' ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. is_regular (add_sheaf_spec U s s') U
[PROOF STEP]
have "(\<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V)"
    if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
obtain V1 r1 f1 where "V1 \<subseteq>U" "is_zariski_open V1" "\<pp> \<in> V1" "r1 \<in> R" "f1 \<in> R" and
        q_V1:"(\<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>V1 r1 f1. \<lbrakk>V1 \<subseteq> U; is_zariski_open V1; \<pp> \<in> V1; r1 \<in> R; f1 \<in> R; \<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>is_regular s U\<close>[unfolded is_regular_def] \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac s V)
\<pp> \<in> U

goal (1 subgoal):
 1. (\<And>V1 r1 f1. \<lbrakk>V1 \<subseteq> U; is_zariski_open V1; \<pp> \<in> V1; r1 \<in> R; f1 \<in> R; \<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
\<pp> \<in> U

goal (1 subgoal):
 1. (\<And>V1 r1 f1. \<lbrakk>V1 \<subseteq> U; is_zariski_open V1; \<pp> \<in> V1; r1 \<in> R; f1 \<in> R; \<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V1 \<subseteq> U
is_zariski_open V1
\<pp> \<in> V1
r1 \<in> R
f1 \<in> R
\<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
obtain V2 r2 f2 where "V2 \<subseteq>U" "is_zariski_open V2" "\<pp> \<in> V2" "r2 \<in> R" "f2 \<in> R" and
        q_V2:"(\<forall>\<qq>. \<qq> \<in> V2 \<longrightarrow> f2 \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r2 f2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>V2 r2 f2. \<lbrakk>V2 \<subseteq> U; is_zariski_open V2; \<pp> \<in> V2; r2 \<in> R; f2 \<in> R; \<forall>\<qq>. \<qq> \<in> V2 \<longrightarrow> f2 \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r2 f2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>is_regular s' U\<close>[unfolded is_regular_def]  \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac s' V)
\<pp> \<in> U

goal (1 subgoal):
 1. (\<And>V2 r2 f2. \<lbrakk>V2 \<subseteq> U; is_zariski_open V2; \<pp> \<in> V2; r2 \<in> R; f2 \<in> R; \<forall>\<qq>. \<qq> \<in> V2 \<longrightarrow> f2 \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r2 f2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
\<pp> \<in> U

goal (1 subgoal):
 1. (\<And>V2 r2 f2. \<lbrakk>V2 \<subseteq> U; is_zariski_open V2; \<pp> \<in> V2; r2 \<in> R; f2 \<in> R; \<forall>\<qq>. \<qq> \<in> V2 \<longrightarrow> f2 \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r2 f2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V2 \<subseteq> U
is_zariski_open V2
\<pp> \<in> V2
r2 \<in> R
f2 \<in> R
\<forall>\<qq>. \<qq> \<in> V2 \<longrightarrow> f2 \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r2 f2

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
define V3 where "V3 = V1 \<inter> V2"
[PROOF STATE]
proof (state)
this:
V3 = V1 \<inter> V2

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
define r3 where "r3 = r1 \<cdot> f2 + r2 \<cdot> f1 "
[PROOF STATE]
proof (state)
this:
r3 = r1 \<cdot> f2 + r2 \<cdot> f1

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
define f3 where "f3 = f1 \<cdot> f2"
[PROOF STATE]
proof (state)
this:
f3 = f1 \<cdot> f2

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
have "V3 \<subseteq>U" "\<pp> \<in> V3" "r3 \<in> R" "f3 \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V3 \<subseteq> U &&& \<pp> \<in> V3) &&& r3 \<in> R &&& f3 \<in> R
[PROOF STEP]
unfolding V3_def r3_def f3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V1 \<inter> V2 \<subseteq> U &&& \<pp> \<in> V1 \<inter> V2) &&& r1 \<cdot> f2 + r2 \<cdot> f1 \<in> R &&& f1 \<cdot> f2 \<in> R
[PROOF STEP]
using \<open>V1 \<subseteq> U\<close> \<open>\<pp> \<in> V1\<close> \<open>V2 \<subseteq> U\<close> \<open>\<pp> \<in> V2\<close> \<open>f1 \<in> R\<close> \<open>f2 \<in> R\<close> \<open>r1 \<in> R\<close> \<open>r2 \<in> R\<close>
[PROOF STATE]
proof (prove)
using this:
V1 \<subseteq> U
\<pp> \<in> V1
V2 \<subseteq> U
\<pp> \<in> V2
f1 \<in> R
f2 \<in> R
r1 \<in> R
r2 \<in> R

goal (1 subgoal):
 1. (V1 \<inter> V2 \<subseteq> U &&& \<pp> \<in> V1 \<inter> V2) &&& r1 \<cdot> f2 + r2 \<cdot> f1 \<in> R &&& f1 \<cdot> f2 \<in> R
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
have "is_zariski_open V3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zariski_open V3
[PROOF STEP]
using \<open>is_zariski_open V1\<close> \<open>is_zariski_open V2\<close> topological_space.open_inter
[PROOF STATE]
proof (prove)
using this:
is_zariski_open V1
is_zariski_open V2
\<lbrakk>topological_space ?S ?is_open; ?is_open ?U; ?is_open ?V\<rbrakk> \<Longrightarrow> ?is_open (?U \<inter> ?V)

goal (1 subgoal):
 1. is_zariski_open V3
[PROOF STEP]
by (simp add: V3_def)
[PROOF STATE]
proof (state)
this:
is_zariski_open V3

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_zariski_open V3

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
have "f3 \<notin> \<qq>"
        "add_sheaf_spec U s s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3"
        if "\<qq> \<in> V3" for \<qq>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f3 \<notin> \<qq> &&& add_sheaf_spec U s s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. add_sheaf_spec U s s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
interpret q:quotient_ring "R\<setminus>\<qq>" R "(+)" "(\<cdot>)" \<zero>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using \<open>U \<subseteq> Spec\<close> \<open>V3 \<subseteq> U\<close> \<open>\<qq> \<in> V3\<close> quotient_ring_def local.comm_ring_axioms
          pr_ideal.submonoid_pr_ideal spectrum_def
[PROOF STATE]
proof (prove)
using this:
U \<subseteq> Spec
V3 \<subseteq> U
\<qq> \<in> V3
Comm_Ring.quotient_ring ?S ?R ?addition ?multiplication ?zero ?unit \<equiv> comm_ring ?R ?addition ?multiplication ?zero ?unit \<and> submonoid ?S ?R ?multiplication ?unit
comm_ring R (+) (\<cdot>) \<zero> \<one>
pr_ideal ?R ?I ?addition ?multiplication ?zero ?unit \<Longrightarrow> submonoid (?R\<setminus>?I) ?R ?multiplication ?unit
Spec \<equiv> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. add_sheaf_spec U s s' \<qq> = q.frac r3 f3
[PROOF STEP]
have "f1 \<notin> \<qq>" "s \<qq> = q.frac r1 f1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1 \<notin> \<qq> &&& s \<qq> = q.frac r1 f1
[PROOF STEP]
using q_V1 \<open>\<qq> \<in> V3\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1
\<qq> \<in> V3

goal (1 subgoal):
 1. f1 \<notin> \<qq> &&& s \<qq> = q.frac r1 f1
[PROOF STEP]
unfolding V3_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1
\<qq> \<in> V1 \<inter> V2

goal (1 subgoal):
 1. f1 \<notin> \<qq> &&& s \<qq> = q.frac r1 f1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f1 \<notin> \<qq>
s \<qq> = q.frac r1 f1

goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. add_sheaf_spec U s s' \<qq> = q.frac r3 f3
[PROOF STEP]
have "f2 \<notin> \<qq>" "s' \<qq> = q.frac r2 f2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f2 \<notin> \<qq> &&& s' \<qq> = q.frac r2 f2
[PROOF STEP]
using q_V2 \<open>\<qq> \<in> V3\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>\<qq>. \<qq> \<in> V2 \<longrightarrow> f2 \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r2 f2
\<qq> \<in> V3

goal (1 subgoal):
 1. f2 \<notin> \<qq> &&& s' \<qq> = q.frac r2 f2
[PROOF STEP]
unfolding V3_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<qq>. \<qq> \<in> V2 \<longrightarrow> f2 \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r2 f2
\<qq> \<in> V1 \<inter> V2

goal (1 subgoal):
 1. f2 \<notin> \<qq> &&& s' \<qq> = q.frac r2 f2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f2 \<notin> \<qq>
s' \<qq> = q.frac r2 f2

goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. add_sheaf_spec U s s' \<qq> = q.frac r3 f3
[PROOF STEP]
have "q.add_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 \<cdot> f2 + r2 \<cdot> f1) (f1 \<cdot> f2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q.add_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 \<cdot> f2 + r2 \<cdot> f1) (f1 \<cdot> f2)
[PROOF STEP]
apply (rule q.add_rel_frac)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (r1, f1) \<in> R \<times> (R\<setminus>\<qq>)
 2. (r2, f2) \<in> R \<times> (R\<setminus>\<qq>)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r1, f1) \<in> R \<times> (R\<setminus>\<qq>)
[PROOF STEP]
by (simp add: \<open>f1 \<in> R\<close> \<open>f1 \<notin> \<qq>\<close> \<open>r1 \<in> R\<close> \<open>r2 \<in> R\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r2, f2) \<in> R \<times> (R\<setminus>\<qq>)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r2, f2) \<in> R \<times> (R\<setminus>\<qq>)
[PROOF STEP]
using \<open>f2 \<in> R\<close> \<open>f2 \<notin> \<qq>\<close> \<open>r2 \<in> R\<close>
[PROOF STATE]
proof (prove)
using this:
f2 \<in> R
f2 \<notin> \<qq>
r2 \<in> R

goal (1 subgoal):
 1. (r2, f2) \<in> R \<times> (R\<setminus>\<qq>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
q.add_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 \<cdot> f2 + r2 \<cdot> f1) (f1 \<cdot> f2)

goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. add_sheaf_spec U s s' \<qq> = q.frac r3 f3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q.add_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 \<cdot> f2 + r2 \<cdot> f1) (f1 \<cdot> f2)
[PROOF STEP]
have "q.add_rel (s \<qq>) (s' \<qq>) = q.frac r3 f3"
[PROOF STATE]
proof (prove)
using this:
q.add_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 \<cdot> f2 + r2 \<cdot> f1) (f1 \<cdot> f2)

goal (1 subgoal):
 1. q.add_rel (s \<qq>) (s' \<qq>) = q.frac r3 f3
[PROOF STEP]
unfolding r3_def f3_def
[PROOF STATE]
proof (prove)
using this:
q.add_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 \<cdot> f2 + r2 \<cdot> f1) (f1 \<cdot> f2)

goal (1 subgoal):
 1. q.add_rel (s \<qq>) (s' \<qq>) = q.frac (r1 \<cdot> f2 + r2 \<cdot> f1) (f1 \<cdot> f2)
[PROOF STEP]
using \<open>s \<qq> = q.frac r1 f1\<close> \<open>s' \<qq> = q.frac r2 f2\<close>
[PROOF STATE]
proof (prove)
using this:
q.add_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 \<cdot> f2 + r2 \<cdot> f1) (f1 \<cdot> f2)
s \<qq> = q.frac r1 f1
s' \<qq> = q.frac r2 f2

goal (1 subgoal):
 1. q.add_rel (s \<qq>) (s' \<qq>) = q.frac (r1 \<cdot> f2 + r2 \<cdot> f1) (f1 \<cdot> f2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q.add_rel (s \<qq>) (s' \<qq>) = q.frac r3 f3

goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. add_sheaf_spec U s s' \<qq> = q.frac r3 f3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q.add_rel (s \<qq>) (s' \<qq>) = q.frac r3 f3
[PROOF STEP]
show "add_sheaf_spec U s s' \<qq> = q.frac r3 f3"
[PROOF STATE]
proof (prove)
using this:
q.add_rel (s \<qq>) (s' \<qq>) = q.frac r3 f3

goal (1 subgoal):
 1. add_sheaf_spec U s s' \<qq> = q.frac r3 f3
[PROOF STEP]
unfolding add_sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
q.add_rel (s \<qq>) (s' \<qq>) = q.frac r3 f3

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>) (s' \<pp>)) \<qq> = q.frac r3 f3
[PROOF STEP]
using \<open>V3 \<subseteq> U\<close> \<open>\<qq> \<in> V3\<close>
[PROOF STATE]
proof (prove)
using this:
q.add_rel (s \<qq>) (s' \<qq>) = q.frac r3 f3
V3 \<subseteq> U
\<qq> \<in> V3

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>) (s' \<pp>)) \<qq> = q.frac r3 f3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
add_sheaf_spec U s s' \<qq> = q.frac r3 f3

goal (1 subgoal):
 1. f3 \<notin> \<qq>
[PROOF STEP]
show "f3 \<notin> \<qq>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f3 \<notin> \<qq>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<qq> \<in> V3

goal (1 subgoal):
 1. f3 \<notin> \<qq>
[PROOF STEP]
unfolding V3_def f3_def
[PROOF STATE]
proof (prove)
using this:
\<qq> \<in> V1 \<inter> V2

goal (1 subgoal):
 1. f1 \<cdot> f2 \<notin> \<qq>
[PROOF STEP]
using \<open>f1 \<in> R\<close> \<open>f1 \<notin> \<qq>\<close> \<open>f2 \<in> R\<close> \<open>f2 \<notin> \<qq>\<close> q.sub_composition_closed
[PROOF STATE]
proof (prove)
using this:
\<qq> \<in> V1 \<inter> V2
f1 \<in> R
f1 \<notin> \<qq>
f2 \<in> R
f2 \<notin> \<qq>
\<lbrakk>?a \<in> R\<setminus>\<qq>; ?b \<in> R\<setminus>\<qq>\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<in> R\<setminus>\<qq>

goal (1 subgoal):
 1. f1 \<cdot> f2 \<notin> \<qq>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f3 \<notin> \<qq>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> add_sheaf_spec U s s' ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> add_sheaf_spec U s s' ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> add_sheaf_spec U s s' ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
using is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> add_sheaf_spec U s s' ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3
is_locally_frac ?s ?V \<equiv> \<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>?V. f \<notin> \<qq> \<and> ?s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V

goal (1 subgoal):
 1. is_regular (add_sheaf_spec U s s') U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?\<pp>3 \<in> U \<Longrightarrow> add_sheaf_spec U s s' ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> add_sheaf_spec U s s' ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> is_locally_frac (add_sheaf_spec U s s') V

goal (1 subgoal):
 1. is_regular (add_sheaf_spec U s s') U
[PROOF STEP]
unfolding is_regular_def is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> add_sheaf_spec U s s' ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> add_sheaf_spec U s s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f))

goal (1 subgoal):
 1. \<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> add_sheaf_spec U s s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
is_regular (add_sheaf_spec U s s') U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exesort_les_code: "sort_leq (set cs) c1 c2 = exesort_leq cs c1 c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sort_leq (set cs) c1 c2 = exesort_leq cs c1 c2
[PROOF STEP]
by (simp add: execlass_leq_code exesort_leq_def sort_leq_def)


[STATEMENT]
lemma quasi_isometry_on_subset:
  assumes "lambda C-quasi_isometry_on X f"
          "Y \<subseteq> X"
  shows "lambda C-quasi_isometry_on Y f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda C -quasi_isometry_on Y f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry_on X f
Y \<subseteq> X

goal (1 subgoal):
 1. lambda C -quasi_isometry_on Y f
[PROOF STEP]
unfolding quasi_isometry_on_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda \<and> 0 \<le> C \<and> (\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) \<le> lambda * dist x y + C \<and> 1 / lambda * dist x y - C \<le> dist (f x) (f y))
Y \<subseteq> X

goal (1 subgoal):
 1. 1 \<le> lambda \<and> 0 \<le> C \<and> (\<forall>x\<in>Y. \<forall>y\<in>Y. dist (f x) (f y) \<le> lambda * dist x y + C \<and> 1 / lambda * dist x y - C \<le> dist (f x) (f y))
[PROOF STEP]
by auto


[STATEMENT]
theorem psubst_id [simp]: \<open>psubst id = id\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst id = id
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. psubst id x = id x
[PROOF STEP]
fix p :: \<open>('a, 'b) form\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. psubst id x = id x
[PROOF STEP]
show \<open>psubst id p = id p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst id p = id p
[PROOF STEP]
by (induct p) (simp_all add: psubstt_id)
[PROOF STATE]
proof (state)
this:
psubst id p = id p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma new_subc_put:
  \<open>new_term c s \<Longrightarrow> subc c s (subst p t m) = subc c s (subst p (subc_term c s t) m)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m])
[PROOF STEP]
proof (induct p arbitrary: s m t)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>s m t. new_term c s \<Longrightarrow> subc c s (FF[t/m]) = subc c s (FF[subc_term c s t/m])
 2. \<And>s m t. new_term c s \<Longrightarrow> subc c s (TT[t/m]) = subc c s (TT[subc_term c s t/m])
 3. \<And>x1 x2 s m t. new_term c s \<Longrightarrow> subc c s (Pred x1 x2[t/m]) = subc c s (Pred x1 x2[subc_term c s t/m])
 4. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 5. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 6. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Impl p1 p2[t/m]) = subc c s (Impl p1 p2[subc_term c s t/m])
 7. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Neg p[t/m]) = subc c s (Neg p[subc_term c s t/m])
 8. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 9. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
case FF
[PROOF STATE]
proof (state)
this:
new_term c s

goal (9 subgoals):
 1. \<And>s m t. new_term c s \<Longrightarrow> subc c s (FF[t/m]) = subc c s (FF[subc_term c s t/m])
 2. \<And>s m t. new_term c s \<Longrightarrow> subc c s (TT[t/m]) = subc c s (TT[subc_term c s t/m])
 3. \<And>x1 x2 s m t. new_term c s \<Longrightarrow> subc c s (Pred x1 x2[t/m]) = subc c s (Pred x1 x2[subc_term c s t/m])
 4. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 5. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 6. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Impl p1 p2[t/m]) = subc c s (Impl p1 p2[subc_term c s t/m])
 7. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Neg p[t/m]) = subc c s (Neg p[subc_term c s t/m])
 8. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 9. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
new_term c s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
new_term c s

goal (1 subgoal):
 1. subc c s (FF[t/m]) = subc c s (FF[subc_term c s t/m])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
subc c s (FF[t/m]) = subc c s (FF[subc_term c s t/m])

goal (8 subgoals):
 1. \<And>s m t. new_term c s \<Longrightarrow> subc c s (TT[t/m]) = subc c s (TT[subc_term c s t/m])
 2. \<And>x1 x2 s m t. new_term c s \<Longrightarrow> subc c s (Pred x1 x2[t/m]) = subc c s (Pred x1 x2[subc_term c s t/m])
 3. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 4. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 5. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Impl p1 p2[t/m]) = subc c s (Impl p1 p2[subc_term c s t/m])
 6. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Neg p[t/m]) = subc c s (Neg p[subc_term c s t/m])
 7. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 8. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>s m t. new_term c s \<Longrightarrow> subc c s (TT[t/m]) = subc c s (TT[subc_term c s t/m])
 2. \<And>x1 x2 s m t. new_term c s \<Longrightarrow> subc c s (Pred x1 x2[t/m]) = subc c s (Pred x1 x2[subc_term c s t/m])
 3. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 4. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 5. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Impl p1 p2[t/m]) = subc c s (Impl p1 p2[subc_term c s t/m])
 6. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Neg p[t/m]) = subc c s (Neg p[subc_term c s t/m])
 7. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 8. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
case TT
[PROOF STATE]
proof (state)
this:
new_term c s

goal (8 subgoals):
 1. \<And>s m t. new_term c s \<Longrightarrow> subc c s (TT[t/m]) = subc c s (TT[subc_term c s t/m])
 2. \<And>x1 x2 s m t. new_term c s \<Longrightarrow> subc c s (Pred x1 x2[t/m]) = subc c s (Pred x1 x2[subc_term c s t/m])
 3. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 4. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 5. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Impl p1 p2[t/m]) = subc c s (Impl p1 p2[subc_term c s t/m])
 6. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Neg p[t/m]) = subc c s (Neg p[subc_term c s t/m])
 7. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 8. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
new_term c s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
new_term c s

goal (1 subgoal):
 1. subc c s (TT[t/m]) = subc c s (TT[subc_term c s t/m])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
subc c s (TT[t/m]) = subc c s (TT[subc_term c s t/m])

goal (7 subgoals):
 1. \<And>x1 x2 s m t. new_term c s \<Longrightarrow> subc c s (Pred x1 x2[t/m]) = subc c s (Pred x1 x2[subc_term c s t/m])
 2. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 3. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 4. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Impl p1 p2[t/m]) = subc c s (Impl p1 p2[subc_term c s t/m])
 5. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Neg p[t/m]) = subc c s (Neg p[subc_term c s t/m])
 6. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 7. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1 x2 s m t. new_term c s \<Longrightarrow> subc c s (Pred x1 x2[t/m]) = subc c s (Pred x1 x2[subc_term c s t/m])
 2. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 3. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 4. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Impl p1 p2[t/m]) = subc c s (Impl p1 p2[subc_term c s t/m])
 5. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Neg p[t/m]) = subc c s (Neg p[subc_term c s t/m])
 6. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 7. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
case (Pred i l)
[PROOF STATE]
proof (state)
this:
new_term c s

goal (7 subgoals):
 1. \<And>x1 x2 s m t. new_term c s \<Longrightarrow> subc c s (Pred x1 x2[t/m]) = subc c s (Pred x1 x2[subc_term c s t/m])
 2. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 3. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 4. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Impl p1 p2[t/m]) = subc c s (Impl p1 p2[subc_term c s t/m])
 5. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Neg p[t/m]) = subc c s (Neg p[subc_term c s t/m])
 6. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 7. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
new_term c s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
new_term c s

goal (1 subgoal):
 1. subc c s (Pred i l[t/m]) = subc c s (Pred i l[subc_term c s t/m])
[PROOF STEP]
using new_subc_put'
[PROOF STATE]
proof (prove)
using this:
new_term c s
new_term ?c ?s \<Longrightarrow> subc_term ?c ?s (?t[?u/?m]) = subc_term ?c ?s (?t[subc_term ?c ?s ?u/?m])
new_term ?c ?s \<Longrightarrow> subc_list ?c ?s (?l[?u/?m]) = subc_list ?c ?s (?l[subc_term ?c ?s ?u/?m])

goal (1 subgoal):
 1. subc c s (Pred i l[t/m]) = subc c s (Pred i l[subc_term c s t/m])
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
subc c s (Pred i l[t/m]) = subc c s (Pred i l[subc_term c s t/m])

goal (6 subgoals):
 1. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 2. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 3. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Impl p1 p2[t/m]) = subc c s (Impl p1 p2[subc_term c s t/m])
 4. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Neg p[t/m]) = subc c s (Neg p[subc_term c s t/m])
 5. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 6. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 2. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 3. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Impl p1 p2[t/m]) = subc c s (Impl p1 p2[subc_term c s t/m])
 4. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Neg p[t/m]) = subc c s (Neg p[subc_term c s t/m])
 5. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 6. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
case (Neg p)
[PROOF STATE]
proof (state)
this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c s

goal (6 subgoals):
 1. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 2. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 3. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Impl p1 p2[t/m]) = subc c s (Impl p1 p2[subc_term c s t/m])
 4. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Neg p[t/m]) = subc c s (Neg p[subc_term c s t/m])
 5. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 6. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c s

goal (1 subgoal):
 1. subc c s (Neg p[t/m]) = subc c s (Neg p[subc_term c s t/m])
[PROOF STEP]
by (metis subc.simps(4) subst.simps(7))
[PROOF STATE]
proof (state)
this:
subc c s (Neg p[t/m]) = subc c s (Neg p[subc_term c s t/m])

goal (5 subgoals):
 1. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 2. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 3. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Impl p1 p2[t/m]) = subc c s (Impl p1 p2[subc_term c s t/m])
 4. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 5. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 2. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 3. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Impl p1 p2[t/m]) = subc c s (Impl p1 p2[subc_term c s t/m])
 4. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 5. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
case (Impl p q)
[PROOF STATE]
proof (state)
this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c ?s \<Longrightarrow> subc c ?s (q[?t/?m]) = subc c ?s (q[subc_term c ?s ?t/?m])
new_term c s

goal (5 subgoals):
 1. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 2. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 3. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Impl p1 p2[t/m]) = subc c s (Impl p1 p2[subc_term c s t/m])
 4. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 5. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c ?s \<Longrightarrow> subc c ?s (q[?t/?m]) = subc c ?s (q[subc_term c ?s ?t/?m])
new_term c s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c ?s \<Longrightarrow> subc c ?s (q[?t/?m]) = subc c ?s (q[subc_term c ?s ?t/?m])
new_term c s

goal (1 subgoal):
 1. subc c s (Impl p q[t/m]) = subc c s (Impl p q[subc_term c s t/m])
[PROOF STEP]
by (metis subc.simps(5) subst.simps(6))
[PROOF STATE]
proof (state)
this:
subc c s (Impl p q[t/m]) = subc c s (Impl p q[subc_term c s t/m])

goal (4 subgoals):
 1. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 2. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 3. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 4. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 2. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 3. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 4. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
case (Or p q)
[PROOF STATE]
proof (state)
this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c ?s \<Longrightarrow> subc c ?s (q[?t/?m]) = subc c ?s (q[subc_term c ?s ?t/?m])
new_term c s

goal (4 subgoals):
 1. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 2. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Or p1 p2[t/m]) = subc c s (Or p1 p2[subc_term c s t/m])
 3. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 4. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c ?s \<Longrightarrow> subc c ?s (q[?t/?m]) = subc c ?s (q[subc_term c ?s ?t/?m])
new_term c s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c ?s \<Longrightarrow> subc c ?s (q[?t/?m]) = subc c ?s (q[subc_term c ?s ?t/?m])
new_term c s

goal (1 subgoal):
 1. subc c s (Or p q[t/m]) = subc c s (Or p q[subc_term c s t/m])
[PROOF STEP]
by (metis subc.simps(6) subst.simps(5))
[PROOF STATE]
proof (state)
this:
subc c s (Or p q[t/m]) = subc c s (Or p q[subc_term c s t/m])

goal (3 subgoals):
 1. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 2. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 3. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 2. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 3. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
case (And p q)
[PROOF STATE]
proof (state)
this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c ?s \<Longrightarrow> subc c ?s (q[?t/?m]) = subc c ?s (q[subc_term c ?s ?t/?m])
new_term c s

goal (3 subgoals):
 1. \<And>p1 p2 s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p1[t/m]) = subc c s (p1[subc_term c s t/m]); \<And>s m t. new_term c s \<Longrightarrow> subc c s (p2[t/m]) = subc c s (p2[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (And p1 p2[t/m]) = subc c s (And p1 p2[subc_term c s t/m])
 2. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 3. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c ?s \<Longrightarrow> subc c ?s (q[?t/?m]) = subc c ?s (q[subc_term c ?s ?t/?m])
new_term c s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c ?s \<Longrightarrow> subc c ?s (q[?t/?m]) = subc c ?s (q[subc_term c ?s ?t/?m])
new_term c s

goal (1 subgoal):
 1. subc c s (And p q[t/m]) = subc c s (And p q[subc_term c s t/m])
[PROOF STEP]
by (metis subc.simps(7) subst.simps(4))
[PROOF STATE]
proof (state)
this:
subc c s (And p q[t/m]) = subc c s (And p q[subc_term c s t/m])

goal (2 subgoals):
 1. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 2. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 2. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
case (Exists p)
[PROOF STATE]
proof (state)
this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c s

goal (2 subgoals):
 1. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 2. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
have \<open>subc c s (subst (Exists p) (subc_term c s t) m) =
      Exists (subc c (liftt s) (subst p (subc_term c (liftt s) (liftt t)) (Suc m)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subc c s (Exists p[subc_term c s t/m]) = Exists (subc c (liftt s) (p[subc_term c (liftt s) (liftt t)/Suc m]))
[PROOF STEP]
by (simp add: lift_subc)
[PROOF STATE]
proof (state)
this:
subc c s (Exists p[subc_term c s t/m]) = Exists (subc c (liftt s) (p[subc_term c (liftt s) (liftt t)/Suc m]))

goal (2 subgoals):
 1. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 2. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
subc c s (Exists p[subc_term c s t/m]) = Exists (subc c (liftt s) (p[subc_term c (liftt s) (liftt t)/Suc m]))

goal (2 subgoals):
 1. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 2. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
have \<open>\<dots> = Exists (subc c (liftt s) (subst p (liftt t) (Suc m)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Exists (subc c (liftt s) (p[subc_term c (liftt s) (liftt t)/Suc m])) = Exists (subc c (liftt s) (p[liftt t/Suc m]))
[PROOF STEP]
using Exists new_lift(1)
[PROOF STATE]
proof (prove)
using this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c s
new_term ?c ?t \<Longrightarrow> new_term ?c (liftt ?t)

goal (1 subgoal):
 1. Exists (subc c (liftt s) (p[subc_term c (liftt s) (liftt t)/Suc m])) = Exists (subc c (liftt s) (p[liftt t/Suc m]))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Exists (subc c (liftt s) (p[subc_term c (liftt s) (liftt t)/Suc m])) = Exists (subc c (liftt s) (p[liftt t/Suc m]))

goal (2 subgoals):
 1. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
 2. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
subc c s (Exists p[subc_term c s t/m]) = Exists (subc c (liftt s) (p[liftt t/Suc m]))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
subc c s (Exists p[subc_term c s t/m]) = Exists (subc c (liftt s) (p[liftt t/Suc m]))

goal (1 subgoal):
 1. subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
subc c s (Exists p[t/m]) = subc c s (Exists p[subc_term c s t/m])

goal (1 subgoal):
 1. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
[PROOF STEP]
case (Forall p)
[PROOF STATE]
proof (state)
this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c s

goal (1 subgoal):
 1. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
[PROOF STEP]
have \<open>subc c s (subst (Forall p) (subc_term c s t) m) =
      Forall (subc c (liftt s) (subst p (subc_term c (liftt s) (liftt t)) (Suc m)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subc c s (Forall p[subc_term c s t/m]) = Forall (subc c (liftt s) (p[subc_term c (liftt s) (liftt t)/Suc m]))
[PROOF STEP]
by (simp add: lift_subc)
[PROOF STATE]
proof (state)
this:
subc c s (Forall p[subc_term c s t/m]) = Forall (subc c (liftt s) (p[subc_term c (liftt s) (liftt t)/Suc m]))

goal (1 subgoal):
 1. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
subc c s (Forall p[subc_term c s t/m]) = Forall (subc c (liftt s) (p[subc_term c (liftt s) (liftt t)/Suc m]))

goal (1 subgoal):
 1. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
[PROOF STEP]
have \<open>\<dots> = Forall (subc c (liftt s) (subst p (liftt t) (Suc m)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Forall (subc c (liftt s) (p[subc_term c (liftt s) (liftt t)/Suc m])) = Forall (subc c (liftt s) (p[liftt t/Suc m]))
[PROOF STEP]
using Forall new_lift(1)
[PROOF STATE]
proof (prove)
using this:
new_term c ?s \<Longrightarrow> subc c ?s (p[?t/?m]) = subc c ?s (p[subc_term c ?s ?t/?m])
new_term c s
new_term ?c ?t \<Longrightarrow> new_term ?c (liftt ?t)

goal (1 subgoal):
 1. Forall (subc c (liftt s) (p[subc_term c (liftt s) (liftt t)/Suc m])) = Forall (subc c (liftt s) (p[liftt t/Suc m]))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Forall (subc c (liftt s) (p[subc_term c (liftt s) (liftt t)/Suc m])) = Forall (subc c (liftt s) (p[liftt t/Suc m]))

goal (1 subgoal):
 1. \<And>p s m t. \<lbrakk>\<And>s m t. new_term c s \<Longrightarrow> subc c s (p[t/m]) = subc c s (p[subc_term c s t/m]); new_term c s\<rbrakk> \<Longrightarrow> subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
subc c s (Forall p[subc_term c s t/m]) = Forall (subc c (liftt s) (p[liftt t/Suc m]))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
subc c s (Forall p[subc_term c s t/m]) = Forall (subc c (liftt s) (p[liftt t/Suc m]))

goal (1 subgoal):
 1. subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
subc c s (Forall p[t/m]) = subc c s (Forall p[subc_term c s t/m])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [transfer_rule]:
  "((=) ===> rel_state (rel_option (=))) lookup1 mem_lookup1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> local.rel_state (rel_option (=))) local.lookup1 local.mem_lookup1
[PROOF STEP]
unfolding lookup1_def mem_lookup1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> local.rel_state (rel_option (=))) (\<lambda>k. state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m k))) (\<lambda>k. !m_ref1 \<bind> (\<lambda>m. local.mem_lookup m k))
[PROOF STEP]
apply (intro rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x = y \<Longrightarrow> local.rel_state (rel_option (=)) (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x))) (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m y))
[PROOF STEP]
apply (simp add: option.rel_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. local.rel_state (=) (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x))) (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x))
[PROOF STEP]
apply (rule rel_state_ofI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x)) heap
 2. \<And>x. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>heap. local.inv_pair_weak heap \<longrightarrow> success (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x_)) heap
[PROOF STEP]
by (auto 4 4
        simp: mem_lookup_def inv_pair_lengthD1 execute_simps Let_def
        intro: success_bind_executeI success_returnI Array.success_nthI
       )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x_)))
[PROOF STEP]
using pair.lookup_inv(1)
[PROOF STATE]
proof (prove)
using this:
DP_CRelVS.lift_p local.inv_pair_weak (local.lookup1 ?k')

goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x_)))
[PROOF STEP]
unfolding lookup1_def
[PROOF STATE]
proof (prove)
using this:
DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m ?k')))

goal (1 subgoal):
 1. DP_CRelVS.lift_p local.inv_pair_weak (state_of (!m_ref1 \<bind> (\<lambda>m. local.mem_lookup m x_)))
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_pop_min_op_aref: "(hm_pop_min_op, PR_CONST (mop_pm_pop_min prio)) \<in> heapmap_rel \<rightarrow> \<langle>(Id\<times>\<^sub>rId)\<times>\<^sub>rheapmap_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_pop_min_op, PR_CONST (mop_pm_pop_min prio)) \<in> heapmap_rel \<rightarrow> \<langle>(Id \<times>\<^sub>r Id) \<times>\<^sub>r heapmap_rel\<rangle>nres_rel
[PROOF STEP]
unfolding PR_CONST_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_pop_min_op, mop_pm_pop_min prio) \<in> heapmap_rel \<rightarrow> \<langle>(Id \<times>\<^sub>r Id) \<times>\<^sub>r heapmap_rel\<rangle>nres_rel
[PROOF STEP]
apply (intro fun_relI nres_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> heapmap_rel \<Longrightarrow> hm_pop_min_op a \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r heapmap_rel) (mop_pm_pop_min prio a')
[PROOF STEP]
apply (frule heapmap_hmr_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_pop_min_op a \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r heapmap_rel) (mop_pm_pop_min prio a')
[PROOF STEP]
unfolding mop_pm_pop_min_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_pop_min_op a \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r heapmap_rel) (ASSERT (pre_pm_pop_min a') \<bind> (\<lambda>_. PR_CONST (op_pm_pop_min prio) a'))
[PROOF STEP]
apply (intro ASSERT_refine_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op a \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r heapmap_rel) (PR_CONST (op_pm_pop_min prio) a')
[PROOF STEP]
apply (rule heapmap_nres_rel_prodI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op a \<le> \<Down> (UNIV \<times>\<^sub>r hmr_rel) (?h'x5 a a')
 2. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> ?h'x5 a a' \<le> SPEC (\<lambda>(uu_, y). h.heap_invar y)
 3. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op a \<le>\<^sub>n SPEC (\<lambda>(r, hm'). RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r Id) (PR_CONST (op_pm_pop_min prio) a'))
[PROOF STEP]
apply (rule hm_pop_min_op_refine[param_fo, THEN nres_relD]; assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> h.pop_min_op (hmr_\<alpha> a) \<le> SPEC (\<lambda>(uu_, y). h.heap_invar y)
 2. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op a \<le>\<^sub>n SPEC (\<lambda>(r, hm'). RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r Id) (PR_CONST (op_pm_pop_min prio) a'))
[PROOF STEP]
unfolding heapmap_rel_def hmr_rel_def in_br_conv
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a'. \<lbrakk>a' = heapmap_\<alpha> a \<and> heapmap_invar a; hmr_\<alpha> a = hmr_\<alpha> a \<and> hmr_invar a; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> h.pop_min_op (hmr_\<alpha> a) \<le> SPEC (\<lambda>(uu_, y). h.heap_invar y)
 2. \<And>a a'. \<lbrakk>a' = heapmap_\<alpha> a \<and> heapmap_invar a; hmr_\<alpha> a = hmr_\<alpha> a \<and> hmr_invar a; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op a \<le>\<^sub>n SPEC (\<lambda>(r, hm'). RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r Id) (PR_CONST (op_pm_pop_min prio) a'))
[PROOF STEP]
apply (refine_vcg; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. \<lbrakk>a' = heapmap_\<alpha> a \<and> heapmap_invar a; hmr_\<alpha> a = hmr_\<alpha> a \<and> hmr_invar a; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op a \<le>\<^sub>n SPEC (\<lambda>(r, hm'). RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r Id) (PR_CONST (op_pm_pop_min prio) a'))
[PROOF STEP]
apply (refine_vcg hm_pop_min_\<alpha>_correct[THEN leof_trans]; simp split: prod.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma coreflexive_transitive:
  "coreflexive x \<Longrightarrow> transitive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> transitive x
[PROOF STEP]
by (simp add: coreflexive_transitive)


[STATEMENT]
lemma infsuff_LNil [simp]:
  "infsuff A LNil = A\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infsuff A LNil = A\<^sup>\<omega>
[PROOF STEP]
by (simp add: infsuff_def)