[STATEMENT]
lemma resChainI:
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi \<times> pi) set"
  and   lst :: "name list"

  assumes eqvtRel: "eqvt Rel"
  and     Res:     "\<And>R S y. (R, S) \<in> Rel \<Longrightarrow> (<\<nu>y>R, <\<nu>y>S) \<in> Rel"
  and     PRelQ:   "P \<leadsto><Rel> Q"

  shows "(resChain lst) P \<leadsto><Rel> (resChain lst) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resChain lst P \<leadsto><Rel> resChain lst Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. resChain lst P \<leadsto><Rel> resChain lst Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resChain lst P \<leadsto><Rel> resChain lst Q
[PROOF STEP]
proof(induct lst)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. resChain [] P \<leadsto><Rel> resChain [] Q
 2. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
(* Base case *)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. resChain [] P \<leadsto><Rel> resChain [] Q
 2. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
from PRelQ
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto><Rel> Q
[PROOF STEP]
show "resChain [] P \<leadsto><Rel> resChain [] Q"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto><Rel> Q

goal (1 subgoal):
 1. resChain [] P \<leadsto><Rel> resChain [] Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
resChain [] P \<leadsto><Rel> resChain [] Q

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
(* Inductive step *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
fix a lst
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
assume IH: "(resChain lst P) \<leadsto><Rel> (resChain lst Q)"
[PROOF STATE]
proof (state)
this:
resChain lst P \<leadsto><Rel> resChain lst Q

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
resChain lst P \<leadsto><Rel> resChain lst Q

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
from Res
[PROOF STATE]
proof (chain)
picking this:
(?R, ?S) \<in> Rel \<Longrightarrow> (<\<nu>?y>?R, <\<nu>?y>?S) \<in> Rel
[PROOF STEP]
have "\<And>P Q a. (P, Q) \<in> Rel \<Longrightarrow> (<\<nu>a>P, <\<nu>a>Q) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(?R, ?S) \<in> Rel \<Longrightarrow> (<\<nu>?y>?R, <\<nu>?y>?S) \<in> Rel

goal (1 subgoal):
 1. \<And>P Q a. (P, Q) \<in> Rel \<Longrightarrow> (<\<nu>a>P, <\<nu>a>Q) \<in> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
have "Rel \<subseteq> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rel \<subseteq> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Rel \<subseteq> Rel

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
resChain lst P \<leadsto><Rel> resChain lst Q
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel
Rel \<subseteq> Rel
[PROOF STEP]
have "<\<nu>a>(resChain lst P) \<leadsto><Rel> <\<nu>a>(resChain lst Q)"
[PROOF STATE]
proof (prove)
using this:
resChain lst P \<leadsto><Rel> resChain lst Q
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel
Rel \<subseteq> Rel

goal (1 subgoal):
 1. <\<nu>a>resChain lst P \<leadsto><Rel> <\<nu>a>resChain lst Q
[PROOF STEP]
using eqvtRel
[PROOF STATE]
proof (prove)
using this:
resChain lst P \<leadsto><Rel> resChain lst Q
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel
Rel \<subseteq> Rel
eqvt Rel

goal (1 subgoal):
 1. <\<nu>a>resChain lst P \<leadsto><Rel> <\<nu>a>resChain lst Q
[PROOF STEP]
by(rule_tac resPres)
[PROOF STATE]
proof (state)
this:
<\<nu>a>resChain lst P \<leadsto><Rel> <\<nu>a>resChain lst Q

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto><Rel> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
thus "resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q"
[PROOF STATE]
proof (prove)
using this:
<\<nu>a>resChain lst P \<leadsto><Rel> <\<nu>a>resChain lst Q

goal (1 subgoal):
 1. resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
resChain (a # lst) P \<leadsto><Rel> resChain (a # lst) Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
resChain lst P \<leadsto><Rel> resChain lst Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma normalized_dst_ips_def2: "normalized_dst_ips ms = normalized_n_primitive (is_Dst, dst_sel) normalized_cidr_ip ms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalized_dst_ips ms = normalized_n_primitive (is_Dst, dst_sel) normalized_cidr_ip ms
[PROOF STEP]
by(induction ms rule: normalized_dst_ips.induct, simp_all add: normalized_cidr_ip_def)


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> DNE(\<^bold>\<not>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DNE \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DNE \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma wellFoundedLexLessState1:
assumes
  "finite Vbl"
shows
  "wf (lexLessState1 Vbl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (lexLessState1 Vbl)
[PROOF STEP]
unfolding wf_eq_minimal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> lexLessState1 Vbl \<longrightarrow> y \<notin> Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> lexLessState1 Vbl \<longrightarrow> y \<notin> Q)
[PROOF STEP]
show "\<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
fix Q :: "State set" and state :: State
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
assume "state \<in> Q"
[PROOF STATE]
proof (state)
this:
state \<in> Q

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
let ?Q1 = "{M::LiteralTrail. \<exists> state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> (getM state) = M}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
have "\<exists> stateMin \<in> Q. (\<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
proof (cases "?Q1 \<noteq> {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
 2. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
{M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {}

goal (2 subgoals):
 1. {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
 2. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {}
[PROOF STEP]
obtain M::LiteralTrail
          where "M \<in> ?Q1"
[PROOF STATE]
proof (prove)
using this:
{M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {}

goal (1 subgoal):
 1. (\<And>M. M \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (2 subgoals):
 1. {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
 2. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
M \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
[PROOF STEP]
obtain MMin::LiteralTrail
          where "MMin \<in> ?Q1" "\<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> ?Q1"
[PROOF STATE]
proof (prove)
using this:
M \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (1 subgoal):
 1. (\<And>MMin. \<lbrakk>MMin \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}; \<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfLexLessRestricted[of "Vbl"] \<open>finite Vbl\<close>
[PROOF STATE]
proof (prove)
using this:
M \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
finite Vbl \<Longrightarrow> wf (lexLessRestricted Vbl)
finite Vbl

goal (1 subgoal):
 1. (\<And>MMin. \<lbrakk>MMin \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}; \<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding wf_eq_minimal
[PROOF STATE]
proof (prove)
using this:
M \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
finite Vbl \<Longrightarrow> \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> lexLessRestricted Vbl \<longrightarrow> y \<notin> Q)
finite Vbl

goal (1 subgoal):
 1. (\<And>MMin. \<lbrakk>MMin \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}; \<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>MMin. \<lbrakk>\<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = MMin; \<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> (\<forall>state. getSATFlag state = UNDEF \<longrightarrow> state \<in> Q \<longrightarrow> getM state \<noteq> M')\<rbrakk> \<Longrightarrow> thesis; \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> lexLessRestricted Vbl \<longrightarrow> y \<notin> Q); finite Vbl\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (erule_tac x="?Q1" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>MMin. \<lbrakk>\<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = MMin; \<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> (\<forall>state. getSATFlag state = UNDEF \<longrightarrow> state \<in> Q \<longrightarrow> getM state \<noteq> M')\<rbrakk> \<Longrightarrow> thesis; \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M; finite Vbl; (\<exists>x. x \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}) \<longrightarrow> (\<exists>z\<in>{M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}. \<forall>y. (y, z) \<in> lexLessRestricted Vbl \<longrightarrow> y \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M})\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
MMin \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
\<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (2 subgoals):
 1. {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
 2. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
from \<open>MMin \<in> ?Q1\<close>
[PROOF STATE]
proof (chain)
picking this:
MMin \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
[PROOF STEP]
obtain stateMin
          where "stateMin \<in> Q" "(getM stateMin) = MMin" "getSATFlag stateMin = UNDEF"
[PROOF STATE]
proof (prove)
using this:
MMin \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (1 subgoal):
 1. (\<And>stateMin. \<lbrakk>stateMin \<in> Q; getM stateMin = MMin; getSATFlag stateMin = UNDEF\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stateMin \<in> Q
getM stateMin = MMin
getSATFlag stateMin = UNDEF

goal (2 subgoals):
 1. {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
 2. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
have "\<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
fix state'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
show "(state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
assume "(state', stateMin) \<in> lexLessState1 Vbl"
[PROOF STATE]
proof (state)
this:
(state', stateMin) \<in> lexLessState1 Vbl

goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
hence "getSATFlag state' = UNDEF" "(getM state', getM stateMin) \<in> lexLessRestricted Vbl"
[PROOF STATE]
proof (prove)
using this:
(state', stateMin) \<in> lexLessState1 Vbl

goal (1 subgoal):
 1. getSATFlag state' = UNDEF &&& (getM state', getM stateMin) \<in> lexLessRestricted Vbl
[PROOF STEP]
unfolding lexLessState1_def
[PROOF STATE]
proof (prove)
using this:
(state', stateMin) \<in> {(state1, state2). getSATFlag state1 = UNDEF \<and> getSATFlag state2 = UNDEF \<and> (getM state1, getM state2) \<in> lexLessRestricted Vbl}

goal (1 subgoal):
 1. getSATFlag state' = UNDEF &&& (getM state', getM stateMin) \<in> lexLessRestricted Vbl
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getSATFlag state' = UNDEF
(getM state', getM stateMin) \<in> lexLessRestricted Vbl

goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
hence "getM state' \<notin> ?Q1"
[PROOF STATE]
proof (prove)
using this:
getSATFlag state' = UNDEF
(getM state', getM stateMin) \<in> lexLessRestricted Vbl

goal (1 subgoal):
 1. getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
[PROOF STEP]
using \<open>\<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> ?Q1\<close>
[PROOF STATE]
proof (prove)
using this:
getSATFlag state' = UNDEF
(getM state', getM stateMin) \<in> lexLessRestricted Vbl
\<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (1 subgoal):
 1. getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
[PROOF STEP]
using \<open>(getM stateMin) = MMin\<close>
[PROOF STATE]
proof (prove)
using this:
getSATFlag state' = UNDEF
(getM state', getM stateMin) \<in> lexLessRestricted Vbl
\<forall>M'. (M', MMin) \<in> lexLessRestricted Vbl \<longrightarrow> M' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
getM stateMin = MMin

goal (1 subgoal):
 1. getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (1 subgoal):
 1. (state', stateMin) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
thus "state' \<notin> Q"
[PROOF STATE]
proof (prove)
using this:
getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (1 subgoal):
 1. state' \<notin> Q
[PROOF STEP]
using \<open>getSATFlag state' = UNDEF\<close>
[PROOF STATE]
proof (prove)
using this:
getM state' \<notin> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
getSATFlag state' = UNDEF

goal (1 subgoal):
 1. state' \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
state' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal (2 subgoals):
 1. {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
 2. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal (1 subgoal):
 1. \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
using \<open>stateMin \<in> Q\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
stateMin \<in> Q

goal (1 subgoal):
 1. \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal (1 subgoal):
 1. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {}

goal (1 subgoal):
 1. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
have "\<forall>state'. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>state'. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>state'. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
fix state'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>state'. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
show "(state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (state', state) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
assume "(state', state) \<in> lexLessState1 Vbl"
[PROOF STATE]
proof (state)
this:
(state', state) \<in> lexLessState1 Vbl

goal (1 subgoal):
 1. (state', state) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
hence "getSATFlag state = UNDEF"
[PROOF STATE]
proof (prove)
using this:
(state', state) \<in> lexLessState1 Vbl

goal (1 subgoal):
 1. getSATFlag state = UNDEF
[PROOF STEP]
unfolding lexLessState1_def
[PROOF STATE]
proof (prove)
using this:
(state', state) \<in> {(state1, state2). getSATFlag state1 = UNDEF \<and> getSATFlag state2 = UNDEF \<and> (getM state1, getM state2) \<in> lexLessRestricted Vbl}

goal (1 subgoal):
 1. getSATFlag state = UNDEF
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
getSATFlag state = UNDEF

goal (1 subgoal):
 1. (state', state) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
hence "(getM state) \<in> ?Q1"
[PROOF STATE]
proof (prove)
using this:
getSATFlag state = UNDEF

goal (1 subgoal):
 1. getM state \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
[PROOF STEP]
using \<open>state \<in> Q\<close>
[PROOF STATE]
proof (prove)
using this:
getSATFlag state = UNDEF
state \<in> Q

goal (1 subgoal):
 1. getM state \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getM state \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (1 subgoal):
 1. (state', state) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
getM state \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}

goal (1 subgoal):
 1. False
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
getM state \<in> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M}
\<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {}

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

goal (1 subgoal):
 1. (state', state) \<in> lexLessState1 Vbl \<Longrightarrow> state' \<notin> Q
[PROOF STEP]
thus "state' \<notin> Q"
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. state' \<notin> Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
state' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>state'. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal (1 subgoal):
 1. \<not> {M. \<exists>state. state \<in> Q \<and> getSATFlag state = UNDEF \<and> getM state = M} \<noteq> {} \<Longrightarrow> \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>state'. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal (1 subgoal):
 1. \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
using \<open>state \<in> Q\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>state'. (state', state) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
state \<in> Q

goal (1 subgoal):
 1. \<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?state2 \<in> ?Q2 \<Longrightarrow> \<exists>stateMin\<in>?Q2. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> ?Q2

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?state2 \<in> ?Q2 \<Longrightarrow> \<exists>stateMin\<in>?Q2. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> ?Q2

goal (1 subgoal):
 1. \<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>Q state. state \<in> Q \<longrightarrow> (\<exists>stateMin\<in>Q. \<forall>state'. (state', stateMin) \<in> lexLessState1 Vbl \<longrightarrow> state' \<notin> Q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delete_edges_wf: "wf_list_graph G \<Longrightarrow> wf_list_graph (delete_edges G E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_list_graph G \<Longrightarrow> wf_list_graph (FiniteListGraph.delete_edges G E)
[PROOF STEP]
by (induction E arbitrary: G) (auto simp: delete_edge_wf)


[STATEMENT]
lemma delete_edges_set_nodes: "set (nodesL (delete_edges G E)) = set (nodesL G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (nodesL (FiniteListGraph.delete_edges G E)) = set (nodesL G)
[PROOF STEP]
by (induction E arbitrary: G) (auto simp: delete_edge_set_nodes)


[STATEMENT]
lemma Suc_mod_eq[simp]: "[Suc a = Suc b] (mod 2) = [a = b] (mod 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Suc a = Suc b] (mod 2) = [a = b] (mod 2)
[PROOF STEP]
using Suc_eq_plus1_left cong_add_lcancel_nat
[PROOF STATE]
proof (prove)
using this:
Suc ?n = 1 + ?n
[?a + ?x = ?a + ?y] (mod ?n) = [?x = ?y] (mod ?n)

goal (1 subgoal):
 1. [Suc a = Suc b] (mod 2) = [a = b] (mod 2)
[PROOF STEP]
by presburger


[STATEMENT]
lemma domain_subset_carrier[simp]: "domain c \<subseteq> carrier" if "c \<in> charts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain c \<subseteq> carrier
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
c \<in> charts

goal (1 subgoal):
 1. domain c \<subseteq> carrier
[PROOF STEP]
by (auto simp: carrier_def)


[STATEMENT]
theorem wls_swapAbs_involutive2[simp]:
"wlsAbs (us,s) A \<Longrightarrow> ((A $[x \<and> y]_zs) $[y \<and> x]_zs) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlsAbs (us, s) A \<Longrightarrow> A $[x \<and> y]_zs $[y \<and> x]_zs = A
[PROOF STEP]
using wls_swapAbs_sym[of us s A zs x y]
[PROOF STATE]
proof (prove)
using this:
wlsAbs (us, s) A \<Longrightarrow> A $[x \<and> y]_zs = A $[y \<and> x]_zs

goal (1 subgoal):
 1. wlsAbs (us, s) A \<Longrightarrow> A $[x \<and> y]_zs $[y \<and> x]_zs = A
[PROOF STEP]
by auto


[STATEMENT]
lemma wls_freshAbs_swapAbs_compose_aux:
"\<lbrakk>wlsAbs (us,s) A; wlsPar P\<rbrakk> \<Longrightarrow>
 \<forall> x y z. {x,y,z} \<subseteq> varsOfS P xs \<and> freshAbs xs y A \<and> freshAbs xs z A \<longrightarrow>
           ((A $[y \<and> x]_xs) $[z \<and> y]_xs) = (A $[z \<and> x]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wlsAbs (us, s) A; wlsPar P\<rbrakk> \<Longrightarrow> \<forall>x y z. {x, y, z} \<subseteq> varsOfS P xs \<and> freshAbs xs y A \<and> freshAbs xs z A \<longrightarrow> A $[y \<and> x]_xs $[z \<and> y]_xs = A $[z \<and> x]_xs
[PROOF STEP]
apply(erule wlsAbs_fresh_cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wlsPar P \<Longrightarrow> wlsPar P
 2. \<And>x X. \<lbrakk>wlsPar P; wls s X; \<And>ys. x \<notin> varsOfS P ys; \<And>s' Y. Y \<in> termsOfS P s' \<Longrightarrow> fresh us x Y; \<And>usa s' B. B \<in> absOfS P (usa, s') \<Longrightarrow> freshAbs us x B; \<And>rho. rho \<in> envsOfS P \<Longrightarrow> freshEnv us x rho\<rbrakk> \<Longrightarrow> \<forall>xa y z. {xa, y, z} \<subseteq> varsOfS P xs \<and> freshAbs xs y (Abs us x X) \<and> freshAbs xs z (Abs us x X) \<longrightarrow> Abs us x X $[y \<and> xa]_xs $[z \<and> y]_xs = Abs us x X $[z \<and> xa]_xs
[PROOF STEP]
by simp_all (metis fresh_swap_compose sw_def wls_imp_good)


[STATEMENT]
theorem wls_freshAbs_vsubstAbs:
assumes "wlsAbs (us,s) A"
shows "freshAbs zs z (A $[y1 // y]_ys) =
       (((zs = ys \<and> z = y) \<or> freshAbs zs z A) \<and>
        (freshAbs ys y A \<or> (zs \<noteq> ys \<or> z \<noteq> y1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freshAbs zs z (A $[y1 // y]_ys) = ((zs = ys \<and> z = y \<or> freshAbs zs z A) \<and> (freshAbs ys y A \<or> zs \<noteq> ys \<or> z \<noteq> y1))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wlsAbs (us, s) A

goal (1 subgoal):
 1. freshAbs zs z (A $[y1 // y]_ys) = ((zs = ys \<and> z = y \<or> freshAbs zs z A) \<and> (freshAbs ys y A \<or> zs \<noteq> ys \<or> z \<noteq> y1))
[PROOF STEP]
by(simp add: freshAbs_vsubstAbs)


[STATEMENT]
lemma fst_snd_Gauss_Jordan_column_k_iarrays_PA_eq:
shows "fst (snd (Gauss_Jordan_column_k_iarrays_PA (P,i,A) k)) = fst (Gauss_Jordan_column_k_iarrays (i,A) k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_iarrays_PA (P, i, A) k)) = fst (Gauss_Jordan_column_k_iarrays (i, A) k)
[PROOF STEP]
unfolding Gauss_Jordan_column_k_iarrays_PA_def Gauss_Jordan_column_k_iarrays_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (let Pa = fst (P, i, A); ia = fst (snd (P, i, A)); A = snd (snd (P, i, A)) in if vector_all_zero_from_index (ia, column_iarray k A) \<or> ia = nrows_iarray A then (Pa, ia, A) else let Gauss = Gauss_Jordan_in_ij_iarrays_PA (Pa, A) ia k in (fst Gauss, ia + 1, snd Gauss))) = fst (let Aa = snd (i, A); i = fst (i, A) in if vector_all_zero_from_index (i, column_iarray k Aa) \<or> i = nrows_iarray Aa then (i, Aa) else (Suc i, Gauss_Jordan_in_ij_iarrays Aa i k))
[PROOF STEP]
unfolding Let_def snd_conv fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (if vector_all_zero_from_index (i, column_iarray k A) \<or> i = nrows_iarray A then (P, i, A) else (fst (Gauss_Jordan_in_ij_iarrays_PA (P, A) i k), i + 1, snd (Gauss_Jordan_in_ij_iarrays_PA (P, A) i k)))) = fst (if vector_all_zero_from_index (i, column_iarray k A) \<or> i = nrows_iarray A then (i, A) else (Suc i, Gauss_Jordan_in_ij_iarrays A i k))
[PROOF STEP]
by auto


[STATEMENT]
lemma set_nn_integral_cong:
  assumes "M = M'" "A = B" "\<And>x. x \<in> space M \<inter> A \<Longrightarrow> f x = g x"
  shows   "set_nn_integral M A f = set_nn_integral M' B g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_nn_integral M A f = set_nn_integral M' B g
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
M = M'
A = B
?x \<in> space M \<inter> A \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. set_nn_integral M A f = set_nn_integral M' B g
[PROOF STEP]
unfolding assms(1,2)
[PROOF STATE]
proof (prove)
using this:
M' = M'
B = B
?x \<in> space M' \<inter> B \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. set_nn_integral M' B f = set_nn_integral M' B g
[PROOF STEP]
by (intro nn_integral_cong) (auto simp: indicator_def)


[STATEMENT]
lemma (in topology) frontier_closed [iff]:
  "frontier s closed"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frontier s closed
[PROOF STEP]
by (unfold frt_def)
(intro closure_closed core_open closed_diff_open)


[STATEMENT]
theorem main: \<open>(\<turnstile> p) = (\<forall>I. I \<Turnstile> p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<turnstile> p) = (\<forall>I. I \<Turnstile> p)
[PROOF STEP]
using soundness completeness
[PROOF STATE]
proof (prove)
using this:
\<turnstile> ?p \<Longrightarrow> ?I \<Turnstile> ?p
\<forall>I. I \<Turnstile> ?p \<Longrightarrow> \<turnstile> ?p

goal (1 subgoal):
 1. (\<turnstile> p) = (\<forall>I. I \<Turnstile> p)
[PROOF STEP]
by blast


[STATEMENT]
lemma filter_single_zmset: "filter_zmset P {#x#}\<^sub>z = (if P x then {#x#}\<^sub>z else {#}\<^sub>z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_zmset P {#x#}\<^sub>z = (if P x then {#x#}\<^sub>z else {#}\<^sub>z)
[PROOF STEP]
by (rule zmultiset_eqI) simp


[STATEMENT]
theorem pred_bound_size_univ': "invar_vebt t n \<Longrightarrow> u =  2^n \<Longrightarrow>   T\<^sub>p\<^sub>r\<^sub>e\<^sub>d' t x \<le> 2 + lb (lb u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar_vebt t n; u = 2 ^ n\<rbrakk> \<Longrightarrow> real (T\<^sub>p\<^sub>r\<^sub>e\<^sub>d' t x) \<le> 2 + log 2 (log 2 u)
[PROOF STEP]
using pred_bound_height'[of t n x] height_double_log_univ_size[of u n t]
[PROOF STATE]
proof (prove)
using this:
invar_vebt t n \<Longrightarrow> T\<^sub>p\<^sub>r\<^sub>e\<^sub>d' t x \<le> 1 + height t
\<lbrakk>u = 2 ^ n; invar_vebt t n\<rbrakk> \<Longrightarrow> real (height t) \<le> 1 + log 2 (log 2 u)

goal (1 subgoal):
 1. \<lbrakk>invar_vebt t n; u = 2 ^ n\<rbrakk> \<Longrightarrow> real (T\<^sub>p\<^sub>r\<^sub>e\<^sub>d' t x) \<le> 2 + log 2 (log 2 u)
[PROOF STEP]
by simp


[STATEMENT]
lemma hyper_insert_comm: "A \<squnion> \<lfloor>{a}\<rfloor> = \<lfloor>{a}\<rfloor> \<squnion> A \<and> A \<squnion> (\<lfloor>{a}\<rfloor> \<squnion> B) = \<lfloor>{a}\<rfloor> \<squnion> (A \<squnion> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<squnion> \<lfloor>{a}\<rfloor> = \<lfloor>{a}\<rfloor> \<squnion> A \<and> A \<squnion> (\<lfloor>{a}\<rfloor> \<squnion> B) = \<lfloor>{a}\<rfloor> \<squnion> (A \<squnion> B)
[PROOF STEP]
by(simp add:hyperset_defs)


[STATEMENT]
lemma Disj_E:
  assumes A: "insert A H \<turnstile> C" and B: "insert B H \<turnstile> C" shows "insert (A OR B) H \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (A OR B) H \<turnstile> C
[PROOF STEP]
by (metis A B Disj_mono NegNeg_I Peirce)


[STATEMENT]
lemma Disj_cong: "H \<turnstile> A IFF A' \<Longrightarrow> H \<turnstile> B IFF B' \<Longrightarrow> H \<turnstile> A OR B IFF A' OR B'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IFF A'; H \<turnstile> B IFF B'\<rbrakk> \<Longrightarrow> H \<turnstile> A OR B IFF A' OR B'
[PROOF STEP]
by (metis Conj_E1 Conj_E2 Disj_mono Iff_I Iff_def anti_deduction)


[STATEMENT]
lemma wf_termi_call_steps: "wf termi_call_steps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf termi_call_steps
[PROOF STEP]
apply(unfold termi_call_steps_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {((q, t), p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))}
[PROOF STEP]
apply(simp only:wf_iff_no_infinite_down_chain)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>f. \<forall>i. (f (Suc i), f i) \<in> {((q, t), p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))}
[PROOF STEP]
apply(clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<forall>i. (f (Suc i), f i) \<in> {((q, t), p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))} \<Longrightarrow> False
[PROOF STEP]
apply(rename_tac S)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S. \<forall>i. (S (Suc i), S i) \<in> {((q, t), p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))} \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S. \<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i) \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac
 "\<exists>Cs. Cs 0 = [] & (\<forall>i. (body(fst(S i)) # Cs i,snd(S i)) \<rightarrow>\<^sup>*
                        (CALL(fst(S(i+1)))# Cs(i+1), snd(S(i+1))))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
 2. \<And>S. \<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i) \<Longrightarrow> \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S. \<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i) \<Longrightarrow> \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))
 2. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(rule_tac x = "cseq S" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S. \<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i) \<Longrightarrow> cseq S 0 = [] \<and> (\<forall>i. (body (fst (S i)) # cseq S i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # cseq S (i + 1), snd (S (i + 1))))
 2. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S i. \<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i) \<Longrightarrow> (body (fst (S i)) # cseq S i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # (SOME cs. ([body (fst (S i))], snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # cs, snd (S (Suc i)))) @ cseq S i, snd (S (Suc i)))
 2. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule_tac x=i in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i) \<Longrightarrow> (body (fst (S i)) # cseq S i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # (SOME cs. ([body (fst (S i))], snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # cs, snd (S (Suc i)))) @ cseq S i, snd (S (Suc i)))
 2. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S i x y xa ya cs. \<lbrakk>S (Suc i) = (x, y); S i = (xa, ya); body xa \<down> ya; ([body xa], ya) \<rightarrow>\<^sup>* (CALL x # cs, y)\<rbrakk> \<Longrightarrow> (body xa # cseq S i, ya) \<rightarrow>\<^sup>* (CALL x # (SOME cs. ([body xa], ya) \<rightarrow>\<^sup>* (CALL x # cs, y)) @ cseq S i, y)
 2. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(rename_tac q t p s cs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S i q t p s cs. \<lbrakk>S (Suc i) = (q, t); S i = (p, s); body p \<down> s; ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t)\<rbrakk> \<Longrightarrow> (body p # cseq S i, s) \<rightarrow>\<^sup>* (CALL q # (SOME cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t)) @ cseq S i, t)
 2. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule_tac P = "\<lambda>cs.([body p],s) \<rightarrow>\<^sup>* (CALL q# cs, t)" in someI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S i q t p s cs x. \<lbrakk>S (Suc i) = (q, t); S i = (p, s); body p \<down> s; ([body p], s) \<rightarrow>\<^sup>* (CALL q # x, t)\<rbrakk> \<Longrightarrow> (body p # cseq S i, s) \<rightarrow>\<^sup>* (CALL q # x @ cseq S i, t)
 2. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(fastforce dest:app_execs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac
 "\<forall>i. ((body(fst(S i))# Cs i,snd(S i)), (body(fst(S(i+1)))# Cs(i+1), snd(S(i+1)))) : exec1^+")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1)))\<rbrakk> \<Longrightarrow> \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1)))\<rbrakk> \<Longrightarrow> \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+
 2. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(blast intro:rtrancl_into_trancl1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac "\<exists>f. f 0 = ([body(fst(S 0))],snd(S 0)) \<and> (\<forall>i. (f i, f(i+1)) : exec1^+)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+; \<exists>f. f (0::?'a42) = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + (1::?'a42))) \<in> exec1\<^sup>+)\<rbrakk> \<Longrightarrow> False
 2. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>f. f (0::?'a42) = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + (1::?'a42))) \<in> exec1\<^sup>+)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>f. f (0::?'a42) = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + (1::?'a42))) \<in> exec1\<^sup>+)
 2. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+; \<exists>f. f (0::?'a42) = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + (1::?'a42))) \<in> exec1\<^sup>+)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(rule_tac x = "\<lambda>i.(body(fst(S i))#Cs i,snd(S i))" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+\<rbrakk> \<Longrightarrow> (body (fst (S 0)) # Cs 0, snd (S 0)) = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+)
 2. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+; \<exists>f. f 0 = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + 1)) \<in> exec1\<^sup>+)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+; \<exists>f. f 0 = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + 1)) \<in> exec1\<^sup>+)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule_tac x=0 in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs. \<lbrakk>Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+; \<exists>f. f 0 = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + 1)) \<in> exec1\<^sup>+); (case S (Suc 0) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S 0)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(simp add:split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs. \<lbrakk>Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))) \<in> exec1\<^sup>+; \<exists>f. f 0 = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (Suc i)) \<in> exec1\<^sup>+); body (fst (S 0)) \<down> snd (S 0) \<and> (\<exists>cs. ([body (fst (S 0))], snd (S 0)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc 0))) # cs, snd (S (Suc 0))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs f cs. \<lbrakk>Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))) \<in> exec1\<^sup>+; body (fst (S 0)) \<down> snd (S 0); ([body (fst (S 0))], snd (S 0)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc 0))) # cs, snd (S (Suc 0))); f 0 = ([body (fst (S 0))], snd (S 0)); \<forall>i. (f i, f (Suc i)) \<in> exec1\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(drule termi_impl_no_inf_chain)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs f cs. \<lbrakk>Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))) \<in> exec1\<^sup>+; ([body (fst (S 0))], snd (S 0)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc 0))) # cs, snd (S (Suc 0))); f 0 = ([body (fst (S 0))], snd (S 0)); \<forall>i. (f i, f (Suc i)) \<in> exec1\<^sup>+; \<nexists>f. f 0 = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + 1)) \<in> exec1\<^sup>+)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs f cs. \<lbrakk>Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))) \<in> exec1\<^sup>+; ([body (fst (S 0))], snd (S 0)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc 0))) # cs, snd (S (Suc 0))); f 0 = ([body (fst (S 0))], snd (S 0)); \<forall>i. (f i, f (Suc i)) \<in> exec1\<^sup>+; \<forall>f. f 0 = ([body (fst (S 0))], snd (S 0)) \<longrightarrow> (\<exists>i. (f i, f (Suc i)) \<notin> exec1\<^sup>+)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ineffectual_const_get:
  "\<exists> v.  \<forall> \<sigma>\<in>\<S>. get \<sigma> = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v. \<forall>\<sigma>\<in>\<S>. get \<sigma> = v
[PROOF STEP]
using put_get put_inef
[PROOF STATE]
proof (prove)
using this:
get (put ?\<sigma> ?v) = ?v
put ?\<sigma> ?v = ?\<sigma>

goal (1 subgoal):
 1. \<exists>v. \<forall>\<sigma>\<in>\<S>. get \<sigma> = v
[PROOF STEP]
by auto


[STATEMENT]
lemma heap_read_typedI:
  "\<lbrakk> heap_read h ad al v; \<And>T. P,h \<turnstile> ad@al : T \<Longrightarrow> P,h \<turnstile> v :\<le> T \<rbrakk> \<Longrightarrow> heap_read_typed P h ad al v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_read h ad al v; \<And>T. P,h \<turnstile> ad@al : T \<Longrightarrow> P,h \<turnstile> v :\<le> T\<rbrakk> \<Longrightarrow> heap_read_typed P h ad al v
[PROOF STEP]
unfolding heap_read_typed_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_read h ad al v; \<And>T. P,h \<turnstile> ad@al : T \<Longrightarrow> P,h \<turnstile> v :\<le> T\<rbrakk> \<Longrightarrow> heap_read h ad al v \<and> (\<forall>T. P,h \<turnstile> ad@al : T \<longrightarrow> P,h \<turnstile> v :\<le> T)
[PROOF STEP]
by blast


[STATEMENT]
lemma combine_finite_tree :
  assumes "finite_tree t1"
  and     "finite_tree t2"
shows "finite_tree (combine t1 t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (combine t1 t2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite_tree t1
finite_tree t2

goal (1 subgoal):
 1. finite_tree (combine t1 t2)
[PROOF STEP]
unfolding finite_tree_iff combine_set
[PROOF STATE]
proof (prove)
using this:
finite (Prefix_Tree.set t1)
finite (Prefix_Tree.set t2)

goal (1 subgoal):
 1. finite (Prefix_Tree.set t1 \<union> Prefix_Tree.set t2)
[PROOF STEP]
by blast


[STATEMENT]
lemma (in irules) compile_rules:
  assumes "finished rs"
  shows "prules C_info (compile rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prules C_info (Rewriting_Pterm.compile rs)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. fdisjnt (fst |`| Rewriting_Pterm.compile rs) C
 2. distinct all_constructors
 3. fBall (Rewriting_Pterm.compile rs) prule
 4. is_fmap (Rewriting_Pterm.compile rs)
 5. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs)
 6. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))
[PROOF STEP]
show "is_fmap (compile rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_fmap (Rewriting_Pterm.compile rs)
[PROOF STEP]
using fmap
[PROOF STATE]
proof (prove)
using this:
is_fmap rs

goal (1 subgoal):
 1. is_fmap (Rewriting_Pterm.compile rs)
[PROOF STEP]
unfolding compile_def map_prod_def id_apply
[PROOF STATE]
proof (prove)
using this:
is_fmap rs

goal (1 subgoal):
 1. is_fmap ((\<lambda>(x, y). (x, translate_rhs y)) |`| rs)
[PROOF STEP]
by (rule is_fmap_image)
[PROOF STATE]
proof (state)
this:
is_fmap (Rewriting_Pterm.compile rs)

goal (5 subgoals):
 1. fdisjnt (fst |`| Rewriting_Pterm.compile rs) C
 2. distinct all_constructors
 3. fBall (Rewriting_Pterm.compile rs) prule
 4. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs)
 5. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. fdisjnt (fst |`| Rewriting_Pterm.compile rs) C
 2. distinct all_constructors
 3. fBall (Rewriting_Pterm.compile rs) prule
 4. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs)
 5. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))
[PROOF STEP]
show "fdisjnt (fst |`| compile rs) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fdisjnt (fst |`| Rewriting_Pterm.compile rs) C
[PROOF STEP]
unfolding compile_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fdisjnt (fst |`| map_prod id translate_rhs |`| rs) C
[PROOF STEP]
using disjnt
[PROOF STATE]
proof (prove)
using this:
fdisjnt (fst |`| rs) C

goal (1 subgoal):
 1. fdisjnt (fst |`| map_prod id translate_rhs |`| rs) C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fdisjnt (fst |`| Rewriting_Pterm.compile rs) C

goal (4 subgoals):
 1. distinct all_constructors
 2. fBall (Rewriting_Pterm.compile rs) prule
 3. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs)
 4. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. distinct all_constructors
 2. fBall (Rewriting_Pterm.compile rs) prule
 3. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs)
 4. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))
[PROOF STEP]
have
    "fBall (compile rs) prule"
    "fBall (compile rs) (\<lambda>(_, rhs). \<not> shadows_consts rhs)"
    "fBall (compile rs) (\<lambda>(_, rhs). welldefined rhs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fBall (Rewriting_Pterm.compile rs) prule &&& fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> shadows_consts rhs) &&& fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| all_consts)
[PROOF STEP]
proof (safe del: fsubsetI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
fix name rhs
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
assume "(name, rhs) |\<in>| compile rs"
[PROOF STATE]
proof (state)
this:
(name, rhs) |\<in>| Rewriting_Pterm.compile rs

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
(* FIXME clone of compile_correct *)
[PROOF STATE]
proof (state)
this:
(name, rhs) |\<in>| Rewriting_Pterm.compile rs

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(name, rhs) |\<in>| Rewriting_Pterm.compile rs
[PROOF STEP]
obtain irs where "(name, irs) |\<in>| rs" "rhs = translate_rhs irs"
[PROOF STATE]
proof (prove)
using this:
(name, rhs) |\<in>| Rewriting_Pterm.compile rs

goal (1 subgoal):
 1. (\<And>irs. \<lbrakk>(name, irs) |\<in>| rs; rhs = translate_rhs irs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding compile_def
[PROOF STATE]
proof (prove)
using this:
(name, rhs) |\<in>| map_prod id translate_rhs |`| rs

goal (1 subgoal):
 1. (\<And>irs. \<lbrakk>(name, irs) |\<in>| rs; rhs = translate_rhs irs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(name, irs) |\<in>| rs
rhs = translate_rhs irs

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
hence "is_fmap irs" "irs \<noteq> {||}" "arity irs = 0"
[PROOF STATE]
proof (prove)
using this:
(name, irs) |\<in>| rs
rhs = translate_rhs irs

goal (1 subgoal):
 1. is_fmap irs &&& irs \<noteq> {||} &&& arity irs = 0
[PROOF STEP]
using assms inner
[PROOF STATE]
proof (prove)
using this:
(name, irs) |\<in>| rs
rhs = translate_rhs irs
finished rs
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))

goal (1 subgoal):
 1. is_fmap irs &&& irs \<noteq> {||} &&& arity irs = 0
[PROOF STEP]
unfolding finished_def
[PROOF STATE]
proof (prove)
using this:
(name, irs) |\<in>| rs
rhs = translate_rhs irs
fBall rs (\<lambda>(uu_, irs). arity irs = 0)
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))

goal (1 subgoal):
 1. is_fmap irs &&& irs \<noteq> {||} &&& arity irs = 0
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
is_fmap irs
irs \<noteq> {||}
arity irs = 0

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_fmap irs
irs \<noteq> {||}
arity irs = 0

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
have "arity_compatibles irs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rewriting_Nterm.arity_compatibles irs
[PROOF STEP]
using \<open>(name, irs) |\<in>| rs\<close> inner
[PROOF STATE]
proof (prove)
using this:
(name, irs) |\<in>| rs
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))

goal (1 subgoal):
 1. Rewriting_Nterm.arity_compatibles irs
[PROOF STEP]
by (blast dest: fpairwiseD)
[PROOF STATE]
proof (state)
this:
Rewriting_Nterm.arity_compatibles irs

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_fmap irs
irs \<noteq> {||}
arity irs = 0
Rewriting_Nterm.arity_compatibles irs
[PROOF STEP]
obtain u where "irs = {| ([], u) |}"
[PROOF STATE]
proof (prove)
using this:
is_fmap irs
irs \<noteq> {||}
arity irs = 0
Rewriting_Nterm.arity_compatibles irs

goal (1 subgoal):
 1. (\<And>u. irs = {|([], u)|} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis arity_zero_shape)
[PROOF STATE]
proof (state)
this:
irs = {|([], u)|}

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
hence "rhs = u" and u: "([], u) |\<in>| irs"
[PROOF STATE]
proof (prove)
using this:
irs = {|([], u)|}

goal (1 subgoal):
 1. rhs = u &&& ([], u) |\<in>| irs
[PROOF STEP]
unfolding \<open>rhs = _\<close> translate_rhs_def
[PROOF STATE]
proof (prove)
using this:
irs = {|([], u)|}

goal (1 subgoal):
 1. (snd \<circ> fthe_elem) irs = u &&& ([], u) |\<in>| irs
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
rhs = u
([], u) |\<in>| irs

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
hence "abs_ish [] u"
[PROOF STATE]
proof (prove)
using this:
rhs = u
([], u) |\<in>| irs

goal (1 subgoal):
 1. abs_ish [] u
[PROOF STEP]
using inner \<open>(name, irs) |\<in>| rs\<close>
[PROOF STATE]
proof (prove)
using this:
rhs = u
([], u) |\<in>| irs
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))
(name, irs) |\<in>| rs

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

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
thus "is_abs rhs"
[PROOF STATE]
proof (prove)
using this:
abs_ish [] u

goal (1 subgoal):
 1. is_abs rhs
[PROOF STEP]
unfolding abs_ish_def \<open>rhs = u\<close>
[PROOF STATE]
proof (prove)
using this:
[] \<noteq> [] \<or> is_abs u

goal (1 subgoal):
 1. is_abs u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_abs rhs

goal (4 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 4. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
show "wellformed rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pre_strong_term_class.wellformed rhs
[PROOF STEP]
using u \<open>(name, irs) |\<in>| rs\<close> inner
[PROOF STATE]
proof (prove)
using this:
([], u) |\<in>| irs
(name, irs) |\<in>| rs
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))

goal (1 subgoal):
 1. pre_strong_term_class.wellformed rhs
[PROOF STEP]
unfolding \<open>rhs = u\<close>
[PROOF STATE]
proof (prove)
using this:
([], u) |\<in>| irs
(name, irs) |\<in>| rs
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))

goal (1 subgoal):
 1. pre_strong_term_class.wellformed u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pre_strong_term_class.wellformed rhs

goal (3 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 2. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
have "closed_except u {||}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed u
[PROOF STEP]
using u inner \<open>(name, irs) |\<in>| rs\<close>
[PROOF STATE]
proof (prove)
using this:
([], u) |\<in>| irs
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))
(name, irs) |\<in>| rs

goal (1 subgoal):
 1. closed u
[PROOF STEP]
by (metis (mono_tags, lifting) case_prod_conv fbspec freess_empty)
[PROOF STATE]
proof (state)
this:
closed u

goal (3 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 2. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
thus "closed rhs"
[PROOF STATE]
proof (prove)
using this:
closed u

goal (1 subgoal):
 1. closed rhs
[PROOF STEP]
unfolding \<open>rhs = u\<close>
[PROOF STATE]
proof (prove)
using this:
closed u

goal (1 subgoal):
 1. closed u
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
closed rhs

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
closed rhs

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
assume "shadows_consts rhs"
[PROOF STATE]
proof (state)
this:
shadows_consts rhs

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
hence "shadows_consts u"
[PROOF STATE]
proof (prove)
using this:
shadows_consts rhs

goal (1 subgoal):
 1. shadows_consts u
[PROOF STEP]
unfolding compile_def \<open>rhs = u\<close>
[PROOF STATE]
proof (prove)
using this:
shadows_consts u

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

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
shadows_consts u

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
have "\<not> shadows_consts u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> shadows_consts u
[PROOF STEP]
using inner \<open>([], u) |\<in>| irs\<close> \<open>(name, irs) |\<in>| rs\<close>
[PROOF STATE]
proof (prove)
using this:
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))
([], u) |\<in>| irs
(name, irs) |\<in>| rs

goal (1 subgoal):
 1. \<not> shadows_consts u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> shadows_consts u

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
shadows_consts u
\<not> shadows_consts u
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
shadows_consts u
\<not> shadows_consts u

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

goal (1 subgoal):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
shadows_consts rhs \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
have "welldefined u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consts u |\<subseteq>| all_consts
[PROOF STEP]
using fbspec[OF inner \<open>(name, irs) |\<in>| rs\<close>, simplified] \<open>([], u) |\<in>| irs\<close>
[PROOF STATE]
proof (prove)
using this:
Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts)
([], u) |\<in>| irs

goal (1 subgoal):
 1. consts u |\<subseteq>| all_consts
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
consts u |\<subseteq>| all_consts

goal (1 subgoal):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
thus "welldefined rhs"
[PROOF STATE]
proof (prove)
using this:
consts u |\<subseteq>| all_consts

goal (1 subgoal):
 1. consts rhs |\<subseteq>| all_consts
[PROOF STEP]
unfolding \<open>rhs = u\<close> compile_def
[PROOF STATE]
proof (prove)
using this:
consts u |\<subseteq>| all_consts

goal (1 subgoal):
 1. consts u |\<subseteq>| all_consts
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
consts rhs |\<subseteq>| all_consts

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fBall (Rewriting_Pterm.compile rs) prule
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> shadows_consts rhs)
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| all_consts)

goal (4 subgoals):
 1. distinct all_constructors
 2. fBall (Rewriting_Pterm.compile rs) prule
 3. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs)
 4. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))
[PROOF STEP]
thus
    "fBall (compile rs) prule"
    "fBall (compile rs) (\<lambda>(_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| compile rs) rhs)"
    "fBall (compile rs) (\<lambda>(_, rhs). pre_constants.welldefined C_info (fst |`| compile rs) rhs)"
[PROOF STATE]
proof (prove)
using this:
fBall (Rewriting_Pterm.compile rs) prule
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> shadows_consts rhs)
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| all_consts)

goal (1 subgoal):
 1. fBall (Rewriting_Pterm.compile rs) prule &&& fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs) &&& fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))
[PROOF STEP]
unfolding compile_heads
[PROOF STATE]
proof (prove)
using this:
fBall (Rewriting_Pterm.compile rs) prule
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> shadows_consts rhs)
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| all_consts)

goal (1 subgoal):
 1. fBall (Rewriting_Pterm.compile rs) prule &&& fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> shadows_consts rhs) &&& fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| all_consts)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fBall (Rewriting_Pterm.compile rs) prule
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs)
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))

goal (1 subgoal):
 1. distinct all_constructors
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct all_constructors
[PROOF STEP]
show "distinct all_constructors"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct all_constructors
[PROOF STEP]
by (fact distinct_ctr)
[PROOF STATE]
proof (state)
this:
distinct all_constructors

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [simp]: "pc\<^sub>1 + size(compE\<^sub>2 e\<^sub>1) \<le> pc\<^sub>2 \<Longrightarrow> pcs(compxE\<^sub>2 e\<^sub>1 pc\<^sub>1 d\<^sub>1) \<inter> pcs(compxE\<^sub>2 e\<^sub>2 pc\<^sub>2 d\<^sub>2) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc\<^sub>1 + length (compE\<^sub>2 e\<^sub>1) \<le> pc\<^sub>2 \<Longrightarrow> pcs (compxE\<^sub>2 e\<^sub>1 pc\<^sub>1 d\<^sub>1) \<inter> pcs (compxE\<^sub>2 e\<^sub>2 pc\<^sub>2 d\<^sub>2) = {}
[PROOF STEP]
using pcs_subset
[PROOF STATE]
proof (prove)
using this:
pcs (compxE\<^sub>2 ?e ?pc ?d) \<subseteq> {?pc..<?pc + length (compE\<^sub>2 ?e)}
pcs (compxEs\<^sub>2 ?es ?pc ?d) \<subseteq> {?pc..<?pc + length (compEs\<^sub>2 ?es)}

goal (1 subgoal):
 1. pc\<^sub>1 + length (compE\<^sub>2 e\<^sub>1) \<le> pc\<^sub>2 \<Longrightarrow> pcs (compxE\<^sub>2 e\<^sub>1 pc\<^sub>1 d\<^sub>1) \<inter> pcs (compxE\<^sub>2 e\<^sub>2 pc\<^sub>2 d\<^sub>2) = {}
[PROOF STEP]
by fastforce


[STATEMENT]
lemma (in Order) mem_WWa_then:"W \<in> WWa D g a \<Longrightarrow> W \<subseteq> carrier D \<and>
  Worder (Iod D W) \<and> a \<in> W \<and> (\<forall>x\<in>W. a \<preceq> x) \<and>
  (\<forall>x\<in>W. (if (ExPre (Iod D W) x) then  g (Pre (Iod D W) x) = x else
  (if a \<noteq> x then Sup D (segment (Iod D W) x) = x else a = a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W \<in> WWa D g a \<Longrightarrow> W \<subseteq> carrier D \<and> Worder (Iod D W) \<and> a \<in> W \<and> (\<forall>x\<in>W. a \<preceq> x) \<and> (\<forall>x\<in>W. if ExPre (Iod D W) x then g (Pre (Iod D W) x) = x else if a \<noteq> x then Algebra2.Sup D (segment (Iod D W) x) = x else a = a)
[PROOF STEP]
by (simp add:WWa_def Wa_def)