[STATEMENT]
lemma optim_instrs_length:
  assumes "optim_instrs F ret pc \<Sigma>i xs = Some (\<Sigma>o, ys)"
  shows "length xs = length ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
optim_instrs F ret pc \<Sigma>i xs = Some (\<Sigma>o, ys)

goal (1 subgoal):
 1. length xs = length ys
[PROOF STEP]
unfolding optim_instrs_def
[PROOF STATE]
proof (prove)
using this:
map_option (case_prod (\<lambda>(uu_, y). Pair y)) (monadic_fold_map (\<lambda>(pc, \<Sigma>) instr. map_option (\<lambda>(instr', \<Sigma>o). ((Suc pc, \<Sigma>o), instr')) (optim_instr F ret pc instr \<Sigma>)) (pc, \<Sigma>i) xs) = Some (\<Sigma>o, ys)

goal (1 subgoal):
 1. length xs = length ys
[PROOF STEP]
by (auto intro: monadic_fold_map_length)


[STATEMENT]
lemma mod_tree_lemma1:
  fixes x :: "nat tree"
  assumes "\<forall>i\<in>set_tree y. 0 < i"
  shows "x mod (x + y) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x mod (x + y) = x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x mod (x + y) = x
[PROOF STEP]
have "rel_tree (=) (x mod (x + y)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_tree (=) (x mod (x + y)) x
[PROOF STEP]
by applicative_lifting(simp add: assms)
[PROOF STATE]
proof (state)
this:
rel_tree (=) (x mod (x + y)) x

goal (1 subgoal):
 1. x mod (x + y) = x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
rel_tree (=) (x mod (x + y)) x

goal (1 subgoal):
 1. x mod (x + y) = x
[PROOF STEP]
by(unfold tree.rel_eq)
[PROOF STATE]
proof (state)
this:
x mod (x + y) = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ring_transfer[transfer_rule]:
  assumes[transfer_rule]: "bi_unique A" "right_total A"
  shows
    "(
      (A ===> A ===> A) ===>
      A ===>
      (A ===> A ===> A) ===>
      (A ===> A) ===>
      (A ===> A ===> A) ===>
      (=)
    )
    (ring_ow (Collect (Domainp A))) class.ring"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A) ===> (A ===> A ===> A) ===> (=)) (ring_ow (Collect (Domainp A))) class.ring
[PROOF STEP]
unfolding ring_ow_def class.ring_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A) ===> (A ===> A ===> A) ===> (=)) (\<lambda>plus zero minus uminus times. semiring_ow (Collect (Domainp A)) plus times \<and> ab_group_add_ow (Collect (Domainp A)) plus zero minus uminus) (\<lambda>plus zero minus uminus times. class.ab_group_add plus zero minus uminus \<and> class.semiring plus times)
[PROOF STEP]
apply transfer_prover_start
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. Transfer.Rel ((A ===> A ===> A) ===> (A ===> A ===> A) ===> ?Ri11) ?ab11 class.semiring
 2. Transfer.Rel ((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A) ===> ?Rh11) ?aa11 class.ab_group_add
 3. Transfer.Rel (?Rh11 ===> ?Ri11 ===> (=)) ?a11 (\<and>)
 4. (\<lambda>plus zero minus uminus times. semiring_ow (Collect (Domainp A)) plus times \<and> ab_group_add_ow (Collect (Domainp A)) plus zero minus uminus) = (\<lambda>plus zero minus uminus times. ?a11 (?aa11 plus zero minus uminus) (?ab11 plus times))
[PROOF STEP]
apply transfer_step+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>plus zero minus uminus times. semiring_ow (Collect (Domainp A)) plus times \<and> ab_group_add_ow (Collect (Domainp A)) plus zero minus uminus) = (\<lambda>plus zero minus uminus times. ab_group_add_ow (Collect (Domainp A)) plus zero minus uminus \<and> semiring_ow (Collect (Domainp A)) plus times)
[PROOF STEP]
by blast


[STATEMENT]
lemma add_delete_edges: "wf_graph (G::'v graph) \<Longrightarrow> (a,b) \<in> edges G \<Longrightarrow> (a,b) \<notin> fs \<Longrightarrow>
    add_edge a b (delete_edges G (insert (a, b) fs)) = (delete_edges G fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_graph G; (a, b) \<in> edges G; (a, b) \<notin> fs\<rbrakk> \<Longrightarrow> add_edge a b (delete_edges G (insert (a, b) fs)) = delete_edges G fs
[PROOF STEP]
by(auto simp add: delete_edges_simp2 add_edge_def wf_graph_def)

 \<comment> \<open>fully_connected\<close>


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


[STATEMENT]
lemma nat_to_sch_2: "c_fst n mod 7 = 2 \<Longrightarrow> nat_to_sch n = Base_fst"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_fst n mod 7 = 2 \<Longrightarrow> nat_to_sch n = Base_fst
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_fst n mod 7 = 2 \<Longrightarrow> nat_to_sch n = Base_fst
[PROOF STEP]
assume A1: "c_fst n mod 7 = 2"
[PROOF STATE]
proof (state)
this:
c_fst n mod 7 = 2

goal (1 subgoal):
 1. c_fst n mod 7 = 2 \<Longrightarrow> nat_to_sch n = Base_fst
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_fst n mod 7 = 2
[PROOF STEP]
have "nat_to_sch n = (let u=(c_fst n) mod 7; v=c_snd n; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)"
[PROOF STATE]
proof (prove)
using this:
c_fst n mod 7 = 2

goal (1 subgoal):
 1. nat_to_sch n = (let u = c_fst n mod 7; v = c_snd n; v1 = c_fst v; v2 = c_snd v; sch1 = nat_to_sch v1 in Let (nat_to_sch v2) (loc_f u sch1))
[PROOF STEP]
by (simp add: loc_lm_2)
[PROOF STATE]
proof (state)
this:
nat_to_sch n = (let u = c_fst n mod 7; v = c_snd n; v1 = c_fst v; v2 = c_snd v; sch1 = nat_to_sch v1 in Let (nat_to_sch v2) (loc_f u sch1))

goal (1 subgoal):
 1. c_fst n mod 7 = 2 \<Longrightarrow> nat_to_sch n = Base_fst
[PROOF STEP]
with A1
[PROOF STATE]
proof (chain)
picking this:
c_fst n mod 7 = 2
nat_to_sch n = (let u = c_fst n mod 7; v = c_snd n; v1 = c_fst v; v2 = c_snd v; sch1 = nat_to_sch v1 in Let (nat_to_sch v2) (loc_f u sch1))
[PROOF STEP]
show "nat_to_sch n = Base_fst"
[PROOF STATE]
proof (prove)
using this:
c_fst n mod 7 = 2
nat_to_sch n = (let u = c_fst n mod 7; v = c_snd n; v1 = c_fst v; v2 = c_snd v; sch1 = nat_to_sch v1 in Let (nat_to_sch v2) (loc_f u sch1))

goal (1 subgoal):
 1. nat_to_sch n = Base_fst
[PROOF STEP]
by (simp add: Let_def loc_f_def)
[PROOF STATE]
proof (state)
this:
nat_to_sch n = Base_fst

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma loc_upb_lm_2: "(c_fst n) mod 7 > 1 \<Longrightarrow> c_snd n < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < c_fst n mod 7 \<Longrightarrow> c_snd n < n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 < c_fst n mod 7 \<Longrightarrow> c_snd n < n
[PROOF STEP]
assume A1: "c_fst n mod 7 > 1"
[PROOF STATE]
proof (state)
this:
1 < c_fst n mod 7

goal (1 subgoal):
 1. 1 < c_fst n mod 7 \<Longrightarrow> c_snd n < n
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
1 < c_fst n mod 7
[PROOF STEP]
have S1: "1 < c_fst n"
[PROOF STATE]
proof (prove)
using this:
1 < c_fst n mod 7

goal (1 subgoal):
 1. 1 < c_fst n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < c_fst n

goal (1 subgoal):
 1. 1 < c_fst n mod 7 \<Longrightarrow> c_snd n < n
[PROOF STEP]
have S2: "c_fst n \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_fst n \<le> n
[PROOF STEP]
by (rule c_fst_le_arg)
[PROOF STATE]
proof (state)
this:
c_fst n \<le> n

goal (1 subgoal):
 1. 1 < c_fst n mod 7 \<Longrightarrow> c_snd n < n
[PROOF STEP]
from S1 S2
[PROOF STATE]
proof (chain)
picking this:
1 < c_fst n
c_fst n \<le> n
[PROOF STEP]
have S3: "1 < n"
[PROOF STATE]
proof (prove)
using this:
1 < c_fst n
c_fst n \<le> n

goal (1 subgoal):
 1. 1 < n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < n

goal (1 subgoal):
 1. 1 < c_fst n mod 7 \<Longrightarrow> c_snd n < n
[PROOF STEP]
from S3
[PROOF STATE]
proof (chain)
picking this:
1 < n
[PROOF STEP]
have S4: "n>1"
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. 1 < n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < n

goal (1 subgoal):
 1. 1 < c_fst n mod 7 \<Longrightarrow> c_snd n < n
[PROOF STEP]
from S4
[PROOF STATE]
proof (chain)
picking this:
1 < n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. c_snd n < n
[PROOF STEP]
by (rule c_snd_less_arg)
[PROOF STATE]
proof (state)
this:
c_snd n < n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma val_eq_symm: fixes v1::val and v2::val shows "v1 \<sim> v2 \<Longrightarrow> v2 \<sim> v1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v1 \<sim> v2 \<Longrightarrow> v2 \<sim> v1
[PROOF STEP]
unfolding val_eq_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v1 \<sqsubseteq> v2 \<and> v2 \<sqsubseteq> v1 \<Longrightarrow> v2 \<sqsubseteq> v1 \<and> v1 \<sqsubseteq> v2
[PROOF STEP]
by blast


[STATEMENT]
lemma KB4_5:
  assumes \<open>AxB \<le> A\<close> \<open>Ax4 \<le> A\<close>
  shows \<open>A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
have \<open>A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
AxB \<le> A
Ax4 \<le> A

goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))
[PROOF STEP]
by (auto intro: Ax AxB.intros)
[PROOF STATE]
proof (state)
this:
A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))

goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))

goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
have \<open>A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
AxB \<le> A
Ax4 \<le> A

goal (1 subgoal):
 1. A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p
[PROOF STEP]
by (auto intro: K4_L)
[PROOF STATE]
proof (state)
this:
A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p

goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p
[PROOF STEP]
have \<open>A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)\<close>
[PROOF STATE]
proof (prove)
using this:
A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p

goal (1 subgoal):
 1. A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
using K_map
[PROOF STATE]
proof (prove)
using this:
A \<turnstile> L i (L i p) \<^bold>\<longrightarrow> L i p
?A \<turnstile> ?p \<^bold>\<longrightarrow> ?q \<Longrightarrow> ?A \<turnstile> K ?i ?p \<^bold>\<longrightarrow> K ?i ?q

goal (1 subgoal):
 1. A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)

goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))
A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))
A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)

goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
using K_trans R1
[PROOF STATE]
proof (prove)
using this:
A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i (L i p))
A \<turnstile> K i (L i (L i p)) \<^bold>\<longrightarrow> K i (L i p)
?A \<turnstile> (?p \<^bold>\<longrightarrow> ?q) \<^bold>\<longrightarrow> (?q \<^bold>\<longrightarrow> ?r) \<^bold>\<longrightarrow> ?p \<^bold>\<longrightarrow> ?r
\<lbrakk>?A \<turnstile> ?p; ?A \<turnstile> ?p \<^bold>\<longrightarrow> ?q\<rbrakk> \<Longrightarrow> ?A \<turnstile> ?q

goal (1 subgoal):
 1. A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
A \<turnstile> L i p \<^bold>\<longrightarrow> K i (L i p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nsqn_invalidate_eq:
  assumes "dip \<in> kD(rt)"
      and "dests dip = Some rsn"
    shows "nsqn (invalidate rt dests) dip = rsn - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dests dip = Some rsn

goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dests dip = Some rsn\<rbrakk> \<Longrightarrow> nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
dests dip = Some rsn
[PROOF STEP]
obtain dsk hops nhip pre
      where "invalidate rt dests dip = Some (rsn, dsk, inv, hops, nhip, pre)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dests dip = Some rsn

goal (1 subgoal):
 1. (\<And>dsk hops nhip pre. invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding invalidate_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dests dip = Some rsn

goal (1 subgoal):
 1. (\<And>dsk hops nhip pre. (case (rt dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba)) = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)

goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dests dip = Some rsn\<rbrakk> \<Longrightarrow> nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)

goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dests dip = Some rsn\<rbrakk> \<Longrightarrow> nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
from \<open>dip \<in> kD(rt)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
[PROOF STEP]
have "dip \<in> kD(invalidate rt dests)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt

goal (1 subgoal):
 1. dip \<in> kD (invalidate rt dests)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dip \<in> kD (invalidate rt dests)

goal (1 subgoal):
 1. \<lbrakk>dip \<in> kD rt; dests dip = Some rsn\<rbrakk> \<Longrightarrow> nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)
dip \<in> kD (invalidate rt dests)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)
dip \<in> kD (invalidate rt dests)

goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
using \<open>dests dip = Some rsn\<close>
[PROOF STATE]
proof (prove)
using this:
invalidate rt dests dip = Some (rsn, dsk, Aodv_Basic.inv, hops, nhip, pre)
dip \<in> kD (invalidate rt dests)
dests dip = Some rsn

goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = rsn - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nsqn (invalidate rt dests) dip = rsn - 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compatible_up[simp]: "compatible (up\<cdot>x) (up\<cdot>y) \<longleftrightarrow> compatible x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compatible (up\<cdot>x) (up\<cdot>y) = compatible x y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. compatible (up\<cdot>x) (up\<cdot>y) \<Longrightarrow> compatible x y
 2. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
assume "compatible (up\<cdot>x) (up\<cdot>y)"
[PROOF STATE]
proof (state)
this:
compatible (up\<cdot>x) (up\<cdot>y)

goal (2 subgoals):
 1. compatible (up\<cdot>x) (up\<cdot>y) \<Longrightarrow> compatible x y
 2. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
obtain z' where z': "{up\<cdot>x,up\<cdot>y} <<| z'"
[PROOF STATE]
proof (prove)
using this:
compatible (up\<cdot>x) (up\<cdot>y)

goal (1 subgoal):
 1. (\<And>z'. {up\<cdot>x, up\<cdot>y} <<| z' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding compatible_def
[PROOF STATE]
proof (prove)
using this:
Ex ((<<|) {up\<cdot>x, up\<cdot>y})

goal (1 subgoal):
 1. (\<And>z'. {up\<cdot>x, up\<cdot>y} <<| z' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{up\<cdot>x, up\<cdot>y} <<| z'

goal (2 subgoals):
 1. compatible (up\<cdot>x) (up\<cdot>y) \<Longrightarrow> compatible x y
 2. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{up\<cdot>x, up\<cdot>y} <<| z'
[PROOF STEP]
obtain z where  "{up\<cdot>x,up\<cdot>y} <<| up\<cdot>z"
[PROOF STATE]
proof (prove)
using this:
{up\<cdot>x, up\<cdot>y} <<| z'

goal (1 subgoal):
 1. (\<And>z. {up\<cdot>x, up\<cdot>y} <<| up\<cdot>z \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases z') auto
[PROOF STATE]
proof (state)
this:
{up\<cdot>x, up\<cdot>y} <<| up\<cdot>z

goal (2 subgoals):
 1. compatible (up\<cdot>x) (up\<cdot>y) \<Longrightarrow> compatible x y
 2. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
hence "{x,y} <<| z"
[PROOF STATE]
proof (prove)
using this:
{up\<cdot>x, up\<cdot>y} <<| up\<cdot>z

goal (1 subgoal):
 1. {x, y} <<| z
[PROOF STEP]
unfolding is_lub_def
[PROOF STATE]
proof (prove)
using this:
{up\<cdot>x, up\<cdot>y} <| up\<cdot>z \<and> (\<forall>u. {up\<cdot>x, up\<cdot>y} <| u \<longrightarrow> up\<cdot>z \<sqsubseteq> u)

goal (1 subgoal):
 1. {x, y} <| z \<and> (\<forall>u. {x, y} <| u \<longrightarrow> z \<sqsubseteq> u)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>x \<sqsubseteq> z; y \<sqsubseteq> z; \<forall>u. up\<cdot>x \<sqsubseteq> u \<and> up\<cdot>y \<sqsubseteq> u \<longrightarrow> up\<cdot>z \<sqsubseteq> u; x \<sqsubseteq> u; y \<sqsubseteq> u\<rbrakk> \<Longrightarrow> z \<sqsubseteq> u
[PROOF STEP]
by (metis up_below)
[PROOF STATE]
proof (state)
this:
{x, y} <<| z

goal (2 subgoals):
 1. compatible (up\<cdot>x) (up\<cdot>y) \<Longrightarrow> compatible x y
 2. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
thus "compatible x y"
[PROOF STATE]
proof (prove)
using this:
{x, y} <<| z

goal (1 subgoal):
 1. compatible x y
[PROOF STEP]
unfolding compatible_def
[PROOF STATE]
proof (prove)
using this:
{x, y} <<| z

goal (1 subgoal):
 1. Ex ((<<|) {x, y})
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
compatible x y

goal (1 subgoal):
 1. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
assume "compatible x y"
[PROOF STATE]
proof (state)
this:
compatible x y

goal (1 subgoal):
 1. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
compatible x y
[PROOF STEP]
obtain z where z: "{x,y} <<| z"
[PROOF STATE]
proof (prove)
using this:
compatible x y

goal (1 subgoal):
 1. (\<And>z. {x, y} <<| z \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding compatible_def
[PROOF STATE]
proof (prove)
using this:
Ex ((<<|) {x, y})

goal (1 subgoal):
 1. (\<And>z. {x, y} <<| z \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x, y} <<| z

goal (1 subgoal):
 1. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
hence  "{up\<cdot>x,up\<cdot>y} <<| up\<cdot>z"
[PROOF STATE]
proof (prove)
using this:
{x, y} <<| z

goal (1 subgoal):
 1. {up\<cdot>x, up\<cdot>y} <<| up\<cdot>z
[PROOF STEP]
unfolding is_lub_def
[PROOF STATE]
proof (prove)
using this:
{x, y} <| z \<and> (\<forall>u. {x, y} <| u \<longrightarrow> z \<sqsubseteq> u)

goal (1 subgoal):
 1. {up\<cdot>x, up\<cdot>y} <| up\<cdot>z \<and> (\<forall>u. {up\<cdot>x, up\<cdot>y} <| u \<longrightarrow> up\<cdot>z \<sqsubseteq> u)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>x \<sqsubseteq> z; y \<sqsubseteq> z; \<forall>u. x \<sqsubseteq> u \<and> y \<sqsubseteq> u \<longrightarrow> z \<sqsubseteq> u; up\<cdot>x \<sqsubseteq> u; up\<cdot>y \<sqsubseteq> u\<rbrakk> \<Longrightarrow> up\<cdot>z \<sqsubseteq> u
[PROOF STEP]
by (metis not_up_less_UU upE up_below)
[PROOF STATE]
proof (state)
this:
{up\<cdot>x, up\<cdot>y} <<| up\<cdot>z

goal (1 subgoal):
 1. compatible x y \<Longrightarrow> compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
thus "compatible (up\<cdot>x) (up\<cdot>y)"
[PROOF STATE]
proof (prove)
using this:
{up\<cdot>x, up\<cdot>y} <<| up\<cdot>z

goal (1 subgoal):
 1. compatible (up\<cdot>x) (up\<cdot>y)
[PROOF STEP]
unfolding compatible_def
[PROOF STATE]
proof (prove)
using this:
{up\<cdot>x, up\<cdot>y} <<| up\<cdot>z

goal (1 subgoal):
 1. Ex ((<<|) {up\<cdot>x, up\<cdot>y})
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
compatible (up\<cdot>x) (up\<cdot>y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subst_pp_single: "subst_pp f (Poly_Mapping.single x e) = (f x) ^ e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_pp f (monomial e x) = f x ^ e
[PROOF STEP]
by (simp add: subst_pp_def)


[STATEMENT]
lemma keys_hom_componentD:
  assumes "t \<in> keys (hom_component p n)"
  shows "t \<in> keys p" and "deg_pm t = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> keys p &&& deg_pm t = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t \<in> keys (hom_component p n)

goal (1 subgoal):
 1. t \<in> keys p &&& deg_pm t = n
[PROOF STEP]
by (simp_all add: keys_hom_component)


[STATEMENT]
lemma eqvt_at_apply'':
  assumes "eqvt_at f x"
  shows "(p \<bullet> f) (p \<bullet> x) = f (p \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<bullet> f) (p \<bullet> x) = f (p \<bullet> x)
[PROOF STEP]
by (metis (opaque_lifting, no_types) assms eqvt_at_def permute_fun_def permute_minus_cancel(1))


[STATEMENT]
lemma prv_eql_pls_plus:
"prv (eql (pls (Num m) (Num n))
          (Num (m+n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eql (pls (Num m) (Num n)) (Num (m + n)))
[PROOF STEP]
proof(induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. prv (eql (pls (Num m) (Num 0)) (Num (m + 0)))
 2. \<And>n. prv (eql (pls (Num m) (Num n)) (Num (m + n))) \<Longrightarrow> prv (eql (pls (Num m) (Num (Suc n))) (Num (m + Suc n)))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
prv (eql (pls (Num m) (Num n)) (Num (m + n)))

goal (2 subgoals):
 1. prv (eql (pls (Num m) (Num 0)) (Num (m + 0)))
 2. \<And>n. prv (eql (pls (Num m) (Num n)) (Num (m + n))) \<Longrightarrow> prv (eql (pls (Num m) (Num (Suc n))) (Num (m + Suc n)))
[PROOF STEP]
note 0 = prv_pls_suc[of "Num m" "Num n", simplified]
[PROOF STATE]
proof (state)
this:
prv (eql (pls (Num m) (suc (Num n))) (suc (pls (Num m) (Num n))))

goal (2 subgoals):
 1. prv (eql (pls (Num m) (Num 0)) (Num (m + 0)))
 2. \<And>n. prv (eql (pls (Num m) (Num n)) (Num (m + n))) \<Longrightarrow> prv (eql (pls (Num m) (Num (Suc n))) (Num (m + Suc n)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eql (pls (Num m) (Num (Suc n))) (Num (m + Suc n)))
[PROOF STEP]
by (auto intro: prv_eql_trans[OF _ _ _ 0 prv_suc_cong[OF _ _ Suc]])
[PROOF STATE]
proof (state)
this:
prv (eql (pls (Num m) (Num (Suc n))) (Num (m + Suc n)))

goal (1 subgoal):
 1. prv (eql (pls (Num m) (Num 0)) (Num (m + 0)))
[PROOF STEP]
qed(simp add: prv_pls_zer)


[STATEMENT]
lemma prv_LLq_Num_dsj:  \<comment> \<open>O8\<close>
assumes [simp]: "t \<in> atrm"
shows "prv (dsj (LLq t (Num n)) (LLq (Num n) t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (dsj (LLq t (Num n)) (LLq (Num n) t))
[PROOF STEP]
proof(induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. prv (dsj (LLq t (Num 0)) (LLq (Num 0) t))
 2. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. prv (dsj (LLq t (Num 0)) (LLq (Num 0) t))
 2. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
note prv_LLq_zer[simp]
[PROOF STATE]
proof (state)
this:
?t \<in> atrm \<Longrightarrow> prv (LLq zer ?t)

goal (2 subgoals):
 1. prv (dsj (LLq t (Num 0)) (LLq (Num 0) t))
 2. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (dsj (LLq t (Num 0)) (LLq (Num 0) t))
[PROOF STEP]
by (nprover3 r1: nprv_prvI r2: nprv_dsjIR r3: prv_nprvI)
[PROOF STATE]
proof (state)
this:
prv (dsj (LLq t (Num 0)) (LLq (Num 0) t))

goal (1 subgoal):
 1. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
prv (dsj (LLq t (Num n)) (LLq (Num n) t))

goal (1 subgoal):
 1. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
have nn: "suc (Num n) = Num (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suc (Num n) = Num (Suc n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
suc (Num n) = Num (Suc n)

goal (1 subgoal):
 1. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
have [simp]: "prv (LLq (Num n) (suc (Num n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (LLq (Num n) (suc (Num n)))
[PROOF STEP]
apply(subst nn)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (LLq (Num n) (Num (Suc n)))
[PROOF STEP]
by (rule leq_prv_LLq_Num) simp
[PROOF STATE]
proof (state)
this:
prv (LLq (Num n) (suc (Num n)))

goal (1 subgoal):
 1. \<And>n. prv (dsj (LLq t (Num n)) (LLq (Num n) t)) \<Longrightarrow> prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))
[PROOF STEP]
apply(nrule r: nprv_prvI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
apply(nrule r: nprv_addLemmaE[OF Suc.IH])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {dsj (LLq t (Num n)) (LLq (Num n) t)} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
apply(nrule r: nprv_dsjE0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nprv {LLq t (Num n), dsj (LLq t (Num n)) (LLq (Num n) t)} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
 2. nprv {LLq (Num n) t, dsj (LLq t (Num n)) (LLq (Num n) t)} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {LLq t (Num n), dsj (LLq t (Num n)) (LLq (Num n) t)} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
by (nprover2 r1: nprv_dsjIL r2: O6I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {LLq (Num n) t, dsj (LLq t (Num n)) (LLq (Num n) t)} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {LLq (Num n) t, dsj (LLq t (Num n)) (LLq (Num n) t)} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
apply(nrule r: nprv_clear2_2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
apply(nrule2 r: nprv_eql_Num_casesE[of t n])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nprv {eql t (Num n), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
 2. nprv {neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {eql t (Num n), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
by (nprover3 r1: nprv_dsjIL
      r2: nprv_eql_substE[of _ t "Num n" "LLq (Var xx) (suc (Num n))" xx]
      r3: prv_nprvI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
apply(nrule r: O7E0[of n t])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nprv {eql (Num n) t, neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
 2. nprv {LLq (suc (Num n)) t, neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {eql (Num n) t, neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
by (nprover2 r1: nprv_eql_symE0 r2: nprv_negE01 )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {LLq (suc (Num n)) t, neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {LLq (suc (Num n)) t, neg (eql t (Num n)), LLq (Num n) t} (dsj (LLq t (suc (Num n))) (LLq (suc (Num n)) t))
[PROOF STEP]
by (nrule r: nprv_dsjIR)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prv (dsj (LLq t (Num (Suc n))) (LLq (Num (Suc n)) t))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma less_sets_Un1: "less_sets (A \<union> A') B \<longleftrightarrow> A \<lless> B \<and> A' \<lless> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<union> A' \<lless> B) = (A \<lless> B \<and> A' \<lless> B)
[PROOF STEP]
by (auto simp: less_sets_def)


[STATEMENT]
lemma falsifies\<^sub>g_empty:
  assumes "falsifies\<^sub>g [] C"
  shows "C = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C = {}
[PROOF STEP]
have "\<forall>l \<in> C. False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<in>C. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> C \<Longrightarrow> False
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> C \<Longrightarrow> False
[PROOF STEP]
assume "l\<in>C"
[PROOF STATE]
proof (state)
this:
l \<in> C

goal (1 subgoal):
 1. \<And>l. l \<in> C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<in> C
[PROOF STEP]
have "falsifies\<^sub>l [] l"
[PROOF STATE]
proof (prove)
using this:
l \<in> C

goal (1 subgoal):
 1. falsifies\<^sub>l [] l
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l \<in> C
falsifies\<^sub>g [] C

goal (1 subgoal):
 1. falsifies\<^sub>l [] l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>l [] l

goal (1 subgoal):
 1. \<And>l. l \<in> C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
falsifies\<^sub>l [] l
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
falsifies\<^sub>l [] l

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding falsifies\<^sub>l_def
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l l \<and> (let i = nat_of_fatom (get_atom l) in i < length [] \<and> [] ! i = (\<not> sign l))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>C. False

goal (1 subgoal):
 1. C = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>l\<in>C. False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>C. False

goal (1 subgoal):
 1. C = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma containID:
assumes a:"At i xs \<in># \<Gamma> \<and> At i xs \<in># \<Delta>"
    and b:"Ax \<subseteq> R"
shows "(\<Gamma> \<Rightarrow>* \<Delta>,0) \<in> derivable R*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
At i xs \<in># \<Gamma> \<and> At i xs \<in># \<Delta>
[PROOF STEP]
have "\<Gamma> = \<Gamma> \<ominus> At i xs \<oplus> At i xs \<and> \<Delta> = \<Delta> \<ominus> At i xs \<oplus> At i xs"
[PROOF STATE]
proof (prove)
using this:
At i xs \<in># \<Gamma> \<and> At i xs \<in># \<Delta>

goal (1 subgoal):
 1. \<Gamma> = \<Gamma> \<ominus> At i xs \<oplus> At i xs \<and> \<Delta> = \<Delta> \<ominus> At i xs \<oplus> At i xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Gamma> = \<Gamma> \<ominus> At i xs \<oplus> At i xs \<and> \<Delta> = \<Delta> \<ominus> At i xs \<oplus> At i xs

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> = \<Gamma> \<ominus> At i xs \<oplus> At i xs \<and> \<Delta> = \<Delta> \<ominus> At i xs \<oplus> At i xs
[PROOF STEP]
have "extend ((\<Gamma> \<ominus> At i xs) \<Rightarrow>* (\<Delta> \<ominus> At i xs)) (\<LM> At i xs \<RM> \<Rightarrow>* \<LM> At i xs \<RM>) = (\<Gamma> \<Rightarrow>* \<Delta>)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> = \<Gamma> \<ominus> At i xs \<oplus> At i xs \<and> \<Delta> = \<Delta> \<ominus> At i xs \<oplus> At i xs

goal (1 subgoal):
 1. extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) = ( \<Gamma> \<Rightarrow>* \<Delta>)
[PROOF STEP]
using extend_def[where forms="\<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs" and seq="\<LM>At i xs\<RM> \<Rightarrow>* \<LM>At i xs\<RM>"]
[PROOF STATE]
proof (prove)
using this:
\<Gamma> = \<Gamma> \<ominus> At i xs \<oplus> At i xs \<and> \<Delta> = \<Delta> \<ominus> At i xs \<oplus> At i xs
extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<equiv>  antec ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) + antec ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<Rightarrow>* succ ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) + succ ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>)

goal (1 subgoal):
 1. extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) = ( \<Gamma> \<Rightarrow>* \<Delta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) = ( \<Gamma> \<Rightarrow>* \<Delta>)

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) = ( \<Gamma> \<Rightarrow>* \<Delta>)

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
have "([],\<LM> At i xs \<RM> \<Rightarrow>* \<LM> At i xs \<RM>) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in> R
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
Ax \<subseteq> R

goal (1 subgoal):
 1. ([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in> R

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) = ( \<Gamma> \<Rightarrow>* \<Delta>)
([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in> R
[PROOF STEP]
have "([],\<Gamma> \<Rightarrow>* \<Delta>) \<in> extRules R"
[PROOF STATE]
proof (prove)
using this:
extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) = ( \<Gamma> \<Rightarrow>* \<Delta>)
([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in> R

goal (1 subgoal):
 1. ([],  \<Gamma> \<Rightarrow>* \<Delta>) \<in>  R*
[PROOF STEP]
using extRules.id[where R=R and r="([],  \<LM>At i xs\<RM> \<Rightarrow>* \<LM>At i xs\<RM>)" and S="\<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs"]
       and extendRule_def[where forms="\<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs" and R="([],  \<LM>At i xs\<RM> \<Rightarrow>* \<LM>At i xs\<RM>)"]
[PROOF STATE]
proof (prove)
using this:
extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ( \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) = ( \<Gamma> \<Rightarrow>* \<Delta>)
([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in> R
\<lbrakk>([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in> R; case ([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) of (x, xa) \<Rightarrow> (x, xa) \<in> Ax\<rbrakk> \<Longrightarrow> extendRule ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<in>  R*
extendRule ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) ([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>) \<equiv> (map (extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs)) (fst ([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>)), extend ( \<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs) (snd ([],  \<LM> At i xs  \<RM> \<Rightarrow>* \<LM> At i xs  \<RM>)))

goal (1 subgoal):
 1. ([],  \<Gamma> \<Rightarrow>* \<Delta>) \<in>  R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([],  \<Gamma> \<Rightarrow>* \<Delta>) \<in>  R*

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
([],  \<Gamma> \<Rightarrow>* \<Delta>) \<in>  R*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
([],  \<Gamma> \<Rightarrow>* \<Delta>) \<in>  R*

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
using derivable.base[where R="R*" and C="\<Gamma> \<Rightarrow>* \<Delta>"]
[PROOF STATE]
proof (prove)
using this:
([],  \<Gamma> \<Rightarrow>* \<Delta>) \<in>  R*
([],  \<Gamma> \<Rightarrow>* \<Delta>) \<in>  R* \<Longrightarrow> ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
( \<Gamma> \<Rightarrow>* \<Delta>, 0) \<in> derivable  R*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eVar_simp[simp]:
"eVar MOD xs x = OK (igVar MOD xs x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eVar MOD xs x = OK (igVar MOD xs x)
[PROOF STEP]
unfolding errMOD_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igVar \<lparr>igWls = \<lambda>s eX. case eX of ERR \<Rightarrow> False | OK X \<Rightarrow> igWls MOD s X, igWlsAbs = \<lambda>(us, s) eA. case eA of ERR \<Rightarrow> False | OK A \<Rightarrow> igWlsAbs MOD (us, s) A, igVar = \<lambda>xs x. OK (igVar MOD xs x), igAbs = \<lambda>xs x eX. if eX \<noteq> ERR \<and> (\<exists>s. isInBar (xs, s) \<and> igWls MOD s (check eX)) then OK (igAbs MOD xs x (check eX)) else ERR, igOp = \<lambda>delta einp ebinp. if liftAll (\<lambda>X. X \<noteq> ERR) einp \<and> liftAll (\<lambda>A. A \<noteq> ERR) ebinp \<and> igWlsInp MOD delta (checkI einp) \<and> igWlsBinp MOD delta (checkI ebinp) then OK (igOp MOD delta (checkI einp) (checkI ebinp)) else ERR, igFresh = \<lambda>ys y eX. if eX \<noteq> ERR \<and> (\<exists>s. igWls MOD s (check eX)) then igFresh MOD ys y (check eX) else True, igFreshAbs = \<lambda>ys y eA. if eA \<noteq> ERR \<and> (\<exists>us s. igWlsAbs MOD (us, s) (check eA)) then igFreshAbs MOD ys y (check eA) else True, igSwap = \<lambda>zs z1 z2 eX. if eX \<noteq> ERR \<and> (\<exists>s. igWls MOD s (check eX)) then OK (igSwap MOD zs z1 z2 (check eX)) else ERR, igSwapAbs = \<lambda>zs z1 z2 eA. if eA \<noteq> ERR \<and> (\<exists>us s. igWlsAbs MOD (us, s) (check eA)) then OK (igSwapAbs MOD zs z1 z2 (check eA)) else ERR, igSubst = \<lambda>ys eY y eX. if eY \<noteq> ERR \<and> igWls MOD (asSort ys) (check eY) \<and> eX \<noteq> ERR \<and> (\<exists>s. igWls MOD s (check eX)) then OK (igSubst MOD ys (check eY) y (check eX)) else ERR, igSubstAbs = \<lambda>ys eY y eA. if eY \<noteq> ERR \<and> igWls MOD (asSort ys) (check eY) \<and> eA \<noteq> ERR \<and> (\<exists>us s. igWlsAbs MOD (us, s) (check eA)) then OK (igSubstAbs MOD ys (check eY) y (check eA)) else ERR\<rparr> xs x = OK (igVar MOD xs x)
[PROOF STEP]
by simp


[STATEMENT]
lemma errMOD_igAbsIPresIGWlsSTR:
assumes *: "igAbsIPresIGWls MOD" and **: "igWlsAbsDisj MOD"
and ***: "igWlsAbsIsInBar MOD"
shows "igAbsIPresIGWlsSTR (errMOD MOD)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igAbsIPresIGWlsSTR (errMOD MOD)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
igAbsIPresIGWls MOD
igWlsAbsDisj MOD
igWlsAbsIsInBar MOD

goal (1 subgoal):
 1. igAbsIPresIGWlsSTR (errMOD MOD)
[PROOF STEP]
by (fastforce simp: errMOD_def igAbsIPresIGWls_def igAbsIPresIGWlsSTR_def
igWlsAbsIsInBar_def igWlsAbsDisj_def split: withERR.splits)


[STATEMENT]
lemma errMOD_igSubstAbsIPresIGWlsAbsSTR:
assumes *: "igSubstAbsIPresIGWlsAbs MOD" and **: "igWlsAbsDisj MOD"
and ***: "igWlsAbsIsInBar MOD"
shows "igSubstAbsIPresIGWlsAbsSTR (errMOD MOD)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igSubstAbsIPresIGWlsAbsSTR (errMOD MOD)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
igSubstAbsIPresIGWlsAbs MOD
igWlsAbsDisj MOD
igWlsAbsIsInBar MOD

goal (1 subgoal):
 1. igSubstAbsIPresIGWlsAbsSTR (errMOD MOD)
[PROOF STEP]
by (simp add: errMOD_def igSubstAbsIPresIGWlsAbs_def igSubstAbsIPresIGWlsAbsSTR_def
igWlsAbsIsInBar_def igWlsAbsDisj_def split: withERR.splits) blast


[STATEMENT]
lemma errMOD_igSubstIGAbsSTR:
fixes MOD :: "('index,'bindex,'varSort,'sort,'opSym,'var,'gTerm,'gAbs)model"
assumes *: "igAbsIPresIGWls MOD" and **: "igWlsDisj MOD"
and ***: "igSubstIPresIGWls MOD" and ****: "igSubstIGAbs MOD"
shows "igSubstIGAbsSTR (errMOD MOD)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igSubstIGAbsSTR (errMOD MOD)
[PROOF STEP]
unfolding igSubstIGAbsSTR_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ys y Y xs x X. (xs \<noteq> ys \<or> x \<noteq> y) \<and> eFresh MOD xs x Y \<longrightarrow> eSubstAbs MOD ys Y y (eAbs MOD xs x X) = eAbs MOD xs x (eSubst MOD ys Y y X)
[PROOF STEP]
proof(clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ys y Y xs x X. \<lbrakk>xs \<noteq> ys \<or> x \<noteq> y; eFresh MOD xs x Y\<rbrakk> \<Longrightarrow> eSubstAbs MOD ys Y y (eAbs MOD xs x X) = eAbs MOD xs x (eSubst MOD ys Y y X)
[PROOF STEP]
fix ys xs ::'varSort and y x ::'var and eX eY
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ys y Y xs x X. \<lbrakk>xs \<noteq> ys \<or> x \<noteq> y; eFresh MOD xs x Y\<rbrakk> \<Longrightarrow> eSubstAbs MOD ys Y y (eAbs MOD xs x X) = eAbs MOD xs x (eSubst MOD ys Y y X)
[PROOF STEP]
assume diff: "xs \<noteq> ys \<or> x \<noteq> y"
  and x_fresh_Y: "eFresh MOD xs x eY"
[PROOF STATE]
proof (state)
this:
xs \<noteq> ys \<or> x \<noteq> y
eFresh MOD xs x eY

goal (1 subgoal):
 1. \<And>ys y Y xs x X. \<lbrakk>xs \<noteq> ys \<or> x \<noteq> y; eFresh MOD xs x Y\<rbrakk> \<Longrightarrow> eSubstAbs MOD ys Y y (eAbs MOD xs x X) = eAbs MOD xs x (eSubst MOD ys Y y X)
[PROOF STEP]
show "eSubstAbs MOD ys eY y (eAbs MOD xs x eX) =
        eAbs MOD xs x (eSubst MOD ys eY y eX)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
proof(cases "eX \<noteq> ERR \<and> eY \<noteq> ERR")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eX \<noteq> ERR \<and> eY \<noteq> ERR \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> (eX \<noteq> ERR \<and> eY \<noteq> ERR) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
eX \<noteq> ERR \<and> eY \<noteq> ERR

goal (2 subgoals):
 1. eX \<noteq> ERR \<and> eY \<noteq> ERR \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> (eX \<noteq> ERR \<and> eY \<noteq> ERR) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
define X and Y where "X \<equiv> check eX" and "Y \<equiv> check eY"
[PROOF STATE]
proof (state)
this:
X \<equiv> check eX
Y \<equiv> check eY

goal (2 subgoals):
 1. eX \<noteq> ERR \<and> eY \<noteq> ERR \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> (eX \<noteq> ERR \<and> eY \<noteq> ERR) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
hence eX: "eX = OK X" and eY: "eY = OK Y"
[PROOF STATE]
proof (prove)
using this:
X \<equiv> check eX
Y \<equiv> check eY

goal (1 subgoal):
 1. eX = OK X &&& eY = OK Y
[PROOF STEP]
unfolding X_def Y_def
[PROOF STATE]
proof (prove)
using this:
check eX \<equiv> check eX
check eY \<equiv> check eY

goal (1 subgoal):
 1. eX = OK (check eX) &&& eY = OK (check eY)
[PROOF STEP]
using True OK_check
[PROOF STATE]
proof (prove)
using this:
check eX \<equiv> check eX
check eY \<equiv> check eY
eX \<noteq> ERR \<and> eY \<noteq> ERR
?eX \<noteq> ERR \<Longrightarrow> OK (check ?eX) = ?eX

goal (1 subgoal):
 1. eX = OK (check eX) &&& eY = OK (check eY)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eX = OK X
eY = OK Y

goal (2 subgoals):
 1. eX \<noteq> ERR \<and> eY \<noteq> ERR \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> (eX \<noteq> ERR \<and> eY \<noteq> ERR) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
proof(cases "(\<exists> s. isInBar (xs,s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y

goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y
[PROOF STEP]
obtain s where xs_s: "isInBar (xs, s)" and X: "igWls MOD s X"
      and Y: "igWls MOD (asSort ys) Y"
[PROOF STATE]
proof (prove)
using this:
(\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>isInBar (xs, s); igWls MOD s X; igWls MOD (asSort ys) Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isInBar (xs, s)
igWls MOD s X
igWls MOD (asSort ys) Y

goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
hence "igWlsAbs MOD (xs,s) (igAbs MOD xs x X)"
[PROOF STATE]
proof (prove)
using this:
isInBar (xs, s)
igWls MOD s X
igWls MOD (asSort ys) Y

goal (1 subgoal):
 1. igWlsAbs MOD (xs, s) (igAbs MOD xs x X)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
isInBar (xs, s)
igWls MOD s X
igWls MOD (asSort ys) Y
igAbsIPresIGWls MOD

goal (1 subgoal):
 1. igWlsAbs MOD (xs, s) (igAbs MOD xs x X)
[PROOF STEP]
unfolding igAbsIPresIGWls_def
[PROOF STATE]
proof (prove)
using this:
isInBar (xs, s)
igWls MOD s X
igWls MOD (asSort ys) Y
\<forall>xs s x X. isInBar (xs, s) \<and> igWls MOD s X \<longrightarrow> igWlsAbs MOD (xs, s) (igAbs MOD xs x X)

goal (1 subgoal):
 1. igWlsAbs MOD (xs, s) (igAbs MOD xs x X)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
igWlsAbs MOD (xs, s) (igAbs MOD xs x X)

goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
igWlsAbs MOD (xs, s) (igAbs MOD xs x X)

goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
have "igWls MOD s (igSubst MOD ys Y y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igWls MOD s (igSubst MOD ys Y y X)
[PROOF STEP]
using X Y ***
[PROOF STATE]
proof (prove)
using this:
igWls MOD s X
igWls MOD (asSort ys) Y
igSubstIPresIGWls MOD

goal (1 subgoal):
 1. igWls MOD s (igSubst MOD ys Y y X)
[PROOF STEP]
unfolding igSubstIPresIGWls_def
[PROOF STATE]
proof (prove)
using this:
igWls MOD s X
igWls MOD (asSort ys) Y
\<forall>ys Y y s X. igWls MOD (asSort ys) Y \<and> igWls MOD s X \<longrightarrow> igWls MOD s (igSubst MOD ys Y y X)

goal (1 subgoal):
 1. igWls MOD s (igSubst MOD ys Y y X)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
igWls MOD s (igSubst MOD ys Y y X)

goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
igWls MOD s (igSubst MOD ys Y y X)

goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
have "igFresh MOD xs x Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igFresh MOD xs x Y
[PROOF STEP]
using x_fresh_Y Y
[PROOF STATE]
proof (prove)
using this:
eFresh MOD xs x eY
igWls MOD (asSort ys) Y

goal (1 subgoal):
 1. igFresh MOD xs x Y
[PROOF STEP]
unfolding eY
[PROOF STATE]
proof (prove)
using this:
eFresh MOD xs x (OK Y)
igWls MOD (asSort ys) Y

goal (1 subgoal):
 1. igFresh MOD xs x Y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
igFresh MOD xs x Y

goal (2 subgoals):
 1. (\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
igWlsAbs MOD (xs, s) (igAbs MOD xs x X)
igWls MOD s (igSubst MOD ys Y y X)
igFresh MOD xs x Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
igWlsAbs MOD (xs, s) (igAbs MOD xs x X)
igWls MOD s (igSubst MOD ys Y y X)
igFresh MOD xs x Y

goal (1 subgoal):
 1. eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
unfolding eX eY
[PROOF STATE]
proof (prove)
using this:
igWlsAbs MOD (xs, s) (igAbs MOD xs x X)
igWls MOD s (igSubst MOD ys Y y X)
igFresh MOD xs x Y

goal (1 subgoal):
 1. eSubstAbs MOD ys (OK Y) y (eAbs MOD xs x (OK X)) = eAbs MOD xs x (eSubst MOD ys (OK Y) y (OK X))
[PROOF STEP]
using xs_s X Y
[PROOF STATE]
proof (prove)
using this:
igWlsAbs MOD (xs, s) (igAbs MOD xs x X)
igWls MOD s (igSubst MOD ys Y y X)
igFresh MOD xs x Y
isInBar (xs, s)
igWls MOD s X
igWls MOD (asSort ys) Y

goal (1 subgoal):
 1. eSubstAbs MOD ys (OK Y) y (eAbs MOD xs x (OK X)) = eAbs MOD xs x (eSubst MOD ys (OK Y) y (OK X))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>igWlsAbs MOD (xs, s) (igAbs MOD xs x X); igWls MOD s (igSubst MOD ys Y y X); igFresh MOD xs x Y; isInBar (xs, s); igWls MOD s X; igWls MOD (asSort ys) Y\<rbrakk> \<Longrightarrow> igSubstAbs MOD ys Y y (igAbs MOD xs x X) = igAbs MOD xs x (igSubst MOD ys Y y X)
[PROOF STEP]
using x_fresh_Y diff ****
[PROOF STATE]
proof (prove)
using this:
eFresh MOD xs x eY
xs \<noteq> ys \<or> x \<noteq> y
igSubstIGAbs MOD

goal (1 subgoal):
 1. \<lbrakk>igWlsAbs MOD (xs, s) (igAbs MOD xs x X); igWls MOD s (igSubst MOD ys Y y X); igFresh MOD xs x Y; isInBar (xs, s); igWls MOD s X; igWls MOD (asSort ys) Y\<rbrakk> \<Longrightarrow> igSubstAbs MOD ys Y y (igAbs MOD xs x X) = igAbs MOD xs x (igSubst MOD ys Y y X)
[PROOF STEP]
unfolding igSubstIGAbs_def
[PROOF STATE]
proof (prove)
using this:
eFresh MOD xs x eY
xs \<noteq> ys \<or> x \<noteq> y
\<forall>ys y Y xs x s X. isInBar (xs, s) \<and> igWls MOD (asSort ys) Y \<and> igWls MOD s X \<longrightarrow> (xs \<noteq> ys \<or> x \<noteq> y) \<and> igFresh MOD xs x Y \<longrightarrow> igSubstAbs MOD ys Y y (igAbs MOD xs x X) = igAbs MOD xs x (igSubst MOD ys Y y X)

goal (1 subgoal):
 1. \<lbrakk>igWlsAbs MOD (xs, s) (igAbs MOD xs x X); igWls MOD s (igSubst MOD ys Y y X); igFresh MOD xs x Y; isInBar (xs, s); igWls MOD s X; igWls MOD (asSort ys) Y\<rbrakk> \<Longrightarrow> igSubstAbs MOD ys Y y (igAbs MOD xs x X) = igAbs MOD xs x (igSubst MOD ys Y y X)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)

goal (1 subgoal):
 1. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y)

goal (1 subgoal):
 1. \<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
proof(cases "(EX s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y
[PROOF STEP]
obtain s where X: "igWls MOD s X" and Y: "igWls MOD (asSort ys) Y"
[PROOF STATE]
proof (prove)
using this:
(\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>igWls MOD s X; igWls MOD (asSort ys) Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
igWls MOD s X
igWls MOD (asSort ys) Y

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
hence 2: "~ isInBar (xs,s)"
[PROOF STATE]
proof (prove)
using this:
igWls MOD s X
igWls MOD (asSort ys) Y

goal (1 subgoal):
 1. \<not> isInBar (xs, s)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
igWls MOD s X
igWls MOD (asSort ys) Y
\<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y)

goal (1 subgoal):
 1. \<not> isInBar (xs, s)
[PROOF STEP]
by (auto simp: eX eY)
[PROOF STATE]
proof (state)
this:
\<not> isInBar (xs, s)

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
let ?Xsb = "igSubst MOD ys Y y X"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
have Xsb: "igWls MOD s ?Xsb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igWls MOD s (igSubst MOD ys Y y X)
[PROOF STEP]
using Y X ***
[PROOF STATE]
proof (prove)
using this:
igWls MOD (asSort ys) Y
igWls MOD s X
igSubstIPresIGWls MOD

goal (1 subgoal):
 1. igWls MOD s (igSubst MOD ys Y y X)
[PROOF STEP]
unfolding igSubstIPresIGWls_def
[PROOF STATE]
proof (prove)
using this:
igWls MOD (asSort ys) Y
igWls MOD s X
\<forall>ys Y y s X. igWls MOD (asSort ys) Y \<and> igWls MOD s X \<longrightarrow> igWls MOD s (igSubst MOD ys Y y X)

goal (1 subgoal):
 1. igWls MOD s (igSubst MOD ys Y y X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
igWls MOD s (igSubst MOD ys Y y X)

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
igWls MOD s (igSubst MOD ys Y y X)

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
fix s'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
assume 3: "isInBar (xs,s')" and "igWls MOD s' ?Xsb"
[PROOF STATE]
proof (state)
this:
isInBar (xs, s')
igWls MOD s' (igSubst MOD ys Y y X)

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
hence "s = s'"
[PROOF STATE]
proof (prove)
using this:
isInBar (xs, s')
igWls MOD s' (igSubst MOD ys Y y X)

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using Xsb **
[PROOF STATE]
proof (prove)
using this:
isInBar (xs, s')
igWls MOD s' (igSubst MOD ys Y y X)
igWls MOD s (igSubst MOD ys Y y X)
igWlsDisj MOD

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
unfolding igWlsDisj_def
[PROOF STATE]
proof (prove)
using this:
isInBar (xs, s')
igWls MOD s' (igSubst MOD ys Y y X)
igWls MOD s (igSubst MOD ys Y y X)
\<forall>s s' X. igWls MOD s X \<and> igWls MOD s' X \<longrightarrow> s = s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = s'

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
s = s'

goal (1 subgoal):
 1. False
[PROOF STEP]
using 2 3
[PROOF STATE]
proof (prove)
using this:
s = s'
\<not> isInBar (xs, s)
isInBar (xs, s')

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: eX eY)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>isInBar (xs, ?s'109); igWls MOD ?s'109 (igSubst MOD ys Y y X)\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. (\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
 2. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>isInBar (xs, ?s'109); igWls MOD ?s'109 (igSubst MOD ys Y y X)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
using False Y eAbs_simp2 X eX eY
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>isInBar (xs, ?s'109); igWls MOD ?s'109 (igSubst MOD ys Y y X)\<rbrakk> \<Longrightarrow> False
\<not> ((\<exists>s. isInBar (xs, s) \<and> igWls MOD s X) \<and> igWls MOD (asSort ys) Y)
igWls MOD (asSort ys) Y
\<forall>s. \<not> (isInBar (?xs, s) \<and> igWls ?MOD s ?X) \<Longrightarrow> eAbs ?MOD ?xs ?x (OK ?X) = ERR
igWls MOD s X
eX = OK X
eY = OK Y

goal (1 subgoal):
 1. eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)

goal (1 subgoal):
 1. \<not> ((\<exists>s. igWls MOD s X) \<and> igWls MOD (asSort ys) Y) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
qed(auto simp add: eX eY)
[PROOF STATE]
proof (state)
this:
eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)

goal (1 subgoal):
 1. \<not> (eX \<noteq> ERR \<and> eY \<noteq> ERR) \<Longrightarrow> eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
eSubstAbs MOD ys eY y (eAbs MOD xs x eX) = eAbs MOD xs x (eSubst MOD ys eY y eX)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_of_powers_int: "(x - 1::int) * (\<Sum>i=0..n . x^i) = x ^ Suc n - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x - 1) * sum ((^) x) {0..n} = x ^ Suc n - 1
[PROOF STEP]
by (metis atLeast0AtMost lessThan_Suc_atMost power_diff_1_eq)


[STATEMENT]
lemma vintersection_intersection: "A \<inter>\<^sub>\<circ> B = set (elts A \<inter> elts B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter>\<^sub>\<circ> B = set (elts A \<inter> elts B)
[PROOF STEP]
unfolding inf_V_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (elts A \<inter> elts B) = set (elts A \<inter> elts B)
[PROOF STEP]
by simp


[STATEMENT]
lemma rfoldl_simps[simp]:
    "rfoldl f s [] = RETURN s"
    "rfoldl f s (x#ls) = do { s\<leftarrow>f s x; rfoldl f s ls}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rfoldl f s [] = RETURN s &&& rfoldl f s (x # ls) = f s x \<bind> (\<lambda>s. rfoldl f s ls)
[PROOF STEP]
apply (subst rfoldl.simps, simp)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_all2_leftE:
  assumes "list_all2 P xs ys" "x \<in> set xs"
  obtains y where "y \<in> set ys" "P x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> set ys; P x y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_all2 P xs ys
x \<in> set xs

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> set ys; P x y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by induct auto


[STATEMENT]
lemma (in cring) finsum_reindex_bij_betw:
  assumes "bij_betw h S T" "g \<in> T \<rightarrow> carrier R"
  shows   "finsum R (\<lambda>x. g (h x)) S = finsum R g T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>x\<in>S. g (h x)) = finsum R g T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bij_betw h S T
g \<in> T \<rightarrow> carrier R

goal (1 subgoal):
 1. (\<Oplus>x\<in>S. g (h x)) = finsum R g T
[PROOF STEP]
by (auto simp: bij_betw_def finsum_reindex)


[STATEMENT]
lemma \<tau>diverge_into_\<tau>mredT:
  assumes "\<tau>diverge t (x, shr s)"
  and "thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>" "wset s t = None"
  shows "mthr.\<tau>diverge s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mthr.\<tau>diverge s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<tau>diverge t (x, shr s)
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
wset s t = None

goal (1 subgoal):
 1. mthr.\<tau>diverge s
[PROOF STEP]
proof(coinduction arbitrary: s x)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
case (\<tau>diverge s x)
[PROOF STATE]
proof (state)
this:
\<tau>diverge t (x, shr s)
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
wset s t = None

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
note tst = \<open>thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>\<close>
[PROOF STATE]
proof (state)
this:
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
from \<open>\<tau>diverge t (x, shr s)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<tau>diverge t (x, shr s)
[PROOF STEP]
obtain x' m' where "silent_move t (x, shr s) (x', m')"
    and "\<tau>diverge t (x', m')"
[PROOF STATE]
proof (prove)
using this:
\<tau>diverge t (x, shr s)

goal (1 subgoal):
 1. (\<And>x' m'. \<lbrakk>silent_move t (x, shr s) (x', m'); \<tau>diverge t (x', m')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases auto
[PROOF STATE]
proof (state)
this:
silent_move t (x, shr s) (x', m')
\<tau>diverge t (x', m')

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
from \<open>silent_move t (x, shr s) (x', m')\<close> tst \<open>wset s t = None\<close>
[PROOF STATE]
proof (chain)
picking this:
silent_move t (x, shr s) (x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
wset s t = None
[PROOF STEP]
have "\<tau>mredT s (redT_upd_\<epsilon> s t x' m')"
[PROOF STATE]
proof (prove)
using this:
silent_move t (x, shr s) (x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
wset s t = None

goal (1 subgoal):
 1. \<tau>mredT s (redT_upd_\<epsilon> s t x' m')
[PROOF STEP]
by(rule silent_move_into_RedT_\<tau>_inv)
[PROOF STATE]
proof (state)
this:
\<tau>mredT s (redT_upd_\<epsilon> s t x' m')

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<tau>mredT s (redT_upd_\<epsilon> s t x' m')

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
have "thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>
[PROOF STEP]
using tst
[PROOF STATE]
proof (prove)
using this:
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>

goal (1 subgoal):
 1. thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>
[PROOF STEP]
by(auto simp add: redT_updLns_def)
[PROOF STATE]
proof (state)
this:
thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
have "wset (redT_upd_\<epsilon> s t x' m') t = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wset (redT_upd_\<epsilon> s t x' m') t = None
[PROOF STEP]
using \<open>wset s t = None\<close>
[PROOF STATE]
proof (prove)
using this:
wset s t = None

goal (1 subgoal):
 1. wset (redT_upd_\<epsilon> s t x' m') t = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wset (redT_upd_\<epsilon> s t x' m') t = None

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wset (redT_upd_\<epsilon> s t x' m') t = None

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
from \<open>\<tau>diverge t (x', m')\<close>
[PROOF STATE]
proof (chain)
picking this:
\<tau>diverge t (x', m')
[PROOF STEP]
have "\<tau>diverge t (x', shr (redT_upd_\<epsilon> s t x' m'))"
[PROOF STATE]
proof (prove)
using this:
\<tau>diverge t (x', m')

goal (1 subgoal):
 1. \<tau>diverge t (x', shr (redT_upd_\<epsilon> s t x' m'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<tau>diverge t (x', shr (redT_upd_\<epsilon> s t x' m'))

goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>\<tau>diverge t (xa, shr s); thr s t = \<lfloor>(xa, no_wait_locks)\<rfloor>; wset s t = None\<rbrakk> \<Longrightarrow> \<exists>sa s'. s = sa \<and> \<tau>mredT sa s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<tau>mredT s (redT_upd_\<epsilon> s t x' m')
thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>
wset (redT_upd_\<epsilon> s t x' m') t = None
\<tau>diverge t (x', shr (redT_upd_\<epsilon> s t x' m'))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<tau>mredT s (redT_upd_\<epsilon> s t x' m')
thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>
wset (redT_upd_\<epsilon> s t x' m') t = None
\<tau>diverge t (x', shr (redT_upd_\<epsilon> s t x' m'))

goal (1 subgoal):
 1. \<exists>s s'. s = s \<and> \<tau>mredT s s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
using \<open>\<tau>diverge t (x', m')\<close>
[PROOF STATE]
proof (prove)
using this:
\<tau>mredT s (redT_upd_\<epsilon> s t x' m')
thr (redT_upd_\<epsilon> s t x' m') t = \<lfloor>(x', no_wait_locks)\<rfloor>
wset (redT_upd_\<epsilon> s t x' m') t = None
\<tau>diverge t (x', shr (redT_upd_\<epsilon> s t x' m'))
\<tau>diverge t (x', m')

goal (1 subgoal):
 1. \<exists>s s'. s = s \<and> \<tau>mredT s s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>s s'. s = s \<and> \<tau>mredT s s' \<and> ((\<exists>s x. s' = s \<and> \<tau>diverge t (x, shr s) \<and> thr s t = \<lfloor>(x, no_wait_locks)\<rfloor> \<and> wset s t = None) \<or> mthr.\<tau>diverge s')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma foreachc_reflexive_transitive:
    assumes "reflp r" "transp r"
    assumes "foreach\<^sub>C c f S a\<^sub>1 a\<^sub>2"
    assumes "\<And> x a\<^sub>1 a\<^sub>2. x \<in> S \<Longrightarrow> f x a\<^sub>1 a\<^sub>2 \<Longrightarrow> r a\<^sub>1 a\<^sub>2"
    shows "r a\<^sub>1 a\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a\<^sub>1 a\<^sub>2
[PROOF STEP]
using assms(3, 4)
[PROOF STATE]
proof (prove)
using this:
foreach\<^sub>C c f S a\<^sub>1 a\<^sub>2
\<lbrakk>?x \<in> S; f ?x ?a\<^sub>1 ?a\<^sub>2\<rbrakk> \<Longrightarrow> r ?a\<^sub>1 ?a\<^sub>2

goal (1 subgoal):
 1. r a\<^sub>1 a\<^sub>2
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a. (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> {}; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a a
 2. \<And>S a\<^sub>0 a\<^sub>1 x a\<^sub>2. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; c a\<^sub>1; x \<notin> S; f x a\<^sub>1 a\<^sub>2; \<And>xa a\<^sub>1 a\<^sub>2. \<lbrakk>xa \<in> insert x S; f xa a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>2
 3. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
case (empty a)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> {}; f ?x ?a\<^sub>1 ?a\<^sub>2\<rbrakk> \<Longrightarrow> r ?a\<^sub>1 ?a\<^sub>2

goal (3 subgoals):
 1. \<And>a. (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> {}; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a a
 2. \<And>S a\<^sub>0 a\<^sub>1 x a\<^sub>2. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; c a\<^sub>1; x \<notin> S; f x a\<^sub>1 a\<^sub>2; \<And>xa a\<^sub>1 a\<^sub>2. \<lbrakk>xa \<in> insert x S; f xa a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>2
 3. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a a
[PROOF STEP]
using reflpD assms(1)
[PROOF STATE]
proof (prove)
using this:
reflp ?R \<Longrightarrow> ?R ?x ?x
reflp r

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

goal (2 subgoals):
 1. \<And>S a\<^sub>0 a\<^sub>1 x a\<^sub>2. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; c a\<^sub>1; x \<notin> S; f x a\<^sub>1 a\<^sub>2; \<And>xa a\<^sub>1 a\<^sub>2. \<lbrakk>xa \<in> insert x S; f xa a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>2
 2. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S a\<^sub>0 a\<^sub>1 x a\<^sub>2. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; c a\<^sub>1; x \<notin> S; f x a\<^sub>1 a\<^sub>2; \<And>xa a\<^sub>1 a\<^sub>2. \<lbrakk>xa \<in> insert x S; f xa a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>2
 2. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
case (insert S a\<^sub>0 a\<^sub>1 x a\<^sub>2)
[PROOF STATE]
proof (state)
this:
foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1
(\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1
c a\<^sub>1
x \<notin> S
f x a\<^sub>1 a\<^sub>2
\<lbrakk>?x \<in> insert x S; f ?x ?a\<^sub>1 ?a\<^sub>2\<rbrakk> \<Longrightarrow> r ?a\<^sub>1 ?a\<^sub>2

goal (2 subgoals):
 1. \<And>S a\<^sub>0 a\<^sub>1 x a\<^sub>2. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; c a\<^sub>1; x \<notin> S; f x a\<^sub>1 a\<^sub>2; \<And>xa a\<^sub>1 a\<^sub>2. \<lbrakk>xa \<in> insert x S; f xa a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>2
 2. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
have 0: "r a\<^sub>0 a\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>1
[PROOF STEP]
using insert(2) insert(6)
[PROOF STATE]
proof (prove)
using this:
(\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1
\<lbrakk>?x \<in> insert x S; f ?x ?a\<^sub>1 ?a\<^sub>2\<rbrakk> \<Longrightarrow> r ?a\<^sub>1 ?a\<^sub>2

goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r a\<^sub>0 a\<^sub>1

goal (2 subgoals):
 1. \<And>S a\<^sub>0 a\<^sub>1 x a\<^sub>2. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; c a\<^sub>1; x \<notin> S; f x a\<^sub>1 a\<^sub>2; \<And>xa a\<^sub>1 a\<^sub>2. \<lbrakk>xa \<in> insert x S; f xa a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>2
 2. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
have 1: "r a\<^sub>1 a\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a\<^sub>1 a\<^sub>2
[PROOF STEP]
using insert(6) insert(5)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> insert x S; f ?x ?a\<^sub>1 ?a\<^sub>2\<rbrakk> \<Longrightarrow> r ?a\<^sub>1 ?a\<^sub>2
f x a\<^sub>1 a\<^sub>2

goal (1 subgoal):
 1. r a\<^sub>1 a\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r a\<^sub>1 a\<^sub>2

goal (2 subgoals):
 1. \<And>S a\<^sub>0 a\<^sub>1 x a\<^sub>2. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; c a\<^sub>1; x \<notin> S; f x a\<^sub>1 a\<^sub>2; \<And>xa a\<^sub>1 a\<^sub>2. \<lbrakk>xa \<in> insert x S; f xa a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>2
 2. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>2
[PROOF STEP]
using transpD assms(2) 0 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>transp ?r; ?r ?x ?y; ?r ?y ?z\<rbrakk> \<Longrightarrow> ?r ?x ?z
transp r
r a\<^sub>0 a\<^sub>1
r a\<^sub>1 a\<^sub>2

goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>2
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
r a\<^sub>0 a\<^sub>2

goal (1 subgoal):
 1. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
case (abort S a\<^sub>0 a\<^sub>1 S')
[PROOF STATE]
proof (state)
this:
foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1
(\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1
\<not> c a\<^sub>1
S \<subseteq> S'
\<lbrakk>?x \<in> S'; f ?x ?a\<^sub>1 ?a\<^sub>2\<rbrakk> \<Longrightarrow> r ?a\<^sub>1 ?a\<^sub>2

goal (1 subgoal):
 1. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
have 0: "r a\<^sub>0 a\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>1
[PROOF STEP]
using abort(2) abort(4) abort(5)
[PROOF STATE]
proof (prove)
using this:
(\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1
S \<subseteq> S'
\<lbrakk>?x \<in> S'; f ?x ?a\<^sub>1 ?a\<^sub>2\<rbrakk> \<Longrightarrow> r ?a\<^sub>1 ?a\<^sub>2

goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r a\<^sub>0 a\<^sub>1

goal (1 subgoal):
 1. \<And>S a\<^sub>0 a\<^sub>1 S'. \<lbrakk>foreach\<^sub>C c f S a\<^sub>0 a\<^sub>1; (\<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2) \<Longrightarrow> r a\<^sub>0 a\<^sub>1; \<not> c a\<^sub>1; S \<subseteq> S'; \<And>x a\<^sub>1 a\<^sub>2. \<lbrakk>x \<in> S'; f x a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>1 a\<^sub>2\<rbrakk> \<Longrightarrow> r a\<^sub>0 a\<^sub>1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>1
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
r a\<^sub>0 a\<^sub>1

goal (1 subgoal):
 1. r a\<^sub>0 a\<^sub>1
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
r a\<^sub>0 a\<^sub>1

goal:
No subgoals!
[PROOF STEP]
qed