[STATEMENT]
lemma s_Let_inv[consumes 2, case_names Let1 Let2, elim]:
  assumes "\<lless> \<pi>, Let e\<^sub>1 x e\<^sub>2 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e' \<ggreater>"
  and     "atom x \<sharp> (e\<^sub>1,\<pi>)"
  and     "e' = e\<^sub>2[e\<^sub>1 / x] \<and> value e\<^sub>1 \<and> \<pi> = \<pi>' \<Longrightarrow> Q"
  and     "\<And>e\<^sub>1'. \<lless> \<pi>, e\<^sub>1 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e\<^sub>1' \<ggreater> \<and> e' = Let e\<^sub>1' x e\<^sub>2 \<and> \<not> value e\<^sub>1 \<Longrightarrow> Q"
  shows   "Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lless>\<pi>, Syntax.Let e\<^sub>1 x e\<^sub>2\<ggreater> m\<rightarrow> \<lless>\<pi>', e'\<ggreater>
atom x \<sharp> (e\<^sub>1, \<pi>)
e' = e\<^sub>2[e\<^sub>1 / x] \<and> value e\<^sub>1 \<and> \<pi> = \<pi>' \<Longrightarrow> Q
\<lless>\<pi>, e\<^sub>1\<ggreater> m\<rightarrow> \<lless>\<pi>', ?e\<^sub>1'\<ggreater> \<and> e' = Syntax.Let ?e\<^sub>1' x e\<^sub>2 \<and> \<not> value e\<^sub>1 \<Longrightarrow> Q

goal (1 subgoal):
 1. Q
[PROOF STEP]
by (auto elim: s_Let_inv')


[STATEMENT]
lemma list_len_1_is_singleton: "length l = 1 \<Longrightarrow> (\<exists>x. l = [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length l = 1 \<Longrightarrow> \<exists>x. l = [x]
[PROOF STEP]
by (induct l) auto


[STATEMENT]
lemma eta_reds_appL: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t \<Longrightarrow> s $ u \<rightarrow>\<^sub>\<eta>\<^sup>* t $ u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<rightarrow>\<^sub>\<eta>\<^sup>* t \<Longrightarrow> s $ u \<rightarrow>\<^sub>\<eta>\<^sup>* t $ u
[PROOF STEP]
by (induction s t rule: rtranclp.induct) (auto simp add: rtranclp.rtrancl_into_rtrancl)


[STATEMENT]
lemma tiny_semicategories_vsubset_Vset:
  "set {\<CC>. tiny_semicategory \<alpha> \<CC>} \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.set {\<CC>. tiny_semicategory \<alpha> \<CC>} \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule vsubsetI) (simp add: tiny_semicategory.tiny_smc_in_Vset)


[STATEMENT]
lemma term_variants_pred_inv':
  assumes "term_variants_pred P (Fun f T) t"
  shows "is_Fun t"
    and "length T = length (args t)"
    and "\<And>i. i < length T \<Longrightarrow> term_variants_pred P (T ! i) (args t ! i)"
    and "f \<noteq> the_Fun t \<Longrightarrow> the_Fun t \<in> set (P f)"
    and "P \<equiv> (\<lambda>_. [])(g := [h]) \<Longrightarrow> f \<noteq> the_Fun t \<Longrightarrow> f = g \<and> the_Fun t = h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_Fun t &&& length T = length (args t)) &&& (\<And>i. i < length T \<Longrightarrow> term_variants_pred P (T ! i) (args t ! i)) &&& (f \<noteq> the_Fun t \<Longrightarrow> the_Fun t \<in> set (P f)) &&& (\<lbrakk>P \<equiv> (\<lambda>_. [])(g := [h]); f \<noteq> the_Fun t\<rbrakk> \<Longrightarrow> f = g \<and> the_Fun t = h)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
term_variants_pred P (Fun f T) t

goal (1 subgoal):
 1. (is_Fun t &&& length T = length (args t)) &&& (\<And>i. i < length T \<Longrightarrow> term_variants_pred P (T ! i) (args t ! i)) &&& (f \<noteq> the_Fun t \<Longrightarrow> the_Fun t \<in> set (P f)) &&& (\<lbrakk>P \<equiv> (\<lambda>_. [])(g := [h]); f \<noteq> the_Fun t\<rbrakk> \<Longrightarrow> f = g \<and> the_Fun t = h)
[PROOF STEP]
by (auto elim: term_variants_pred.cases)


[STATEMENT]
lemma term_variants_pred_inv_Var:
  "term_variants_pred P (Var x) t \<longleftrightarrow> t = Var x"
  "term_variants_pred P t (Var x) \<longleftrightarrow> t = Var x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_variants_pred P (Var x) t = (t = Var x) &&& term_variants_pred P t (Var x) = (t = Var x)
[PROOF STEP]
by (auto intro: term_variants_Var elim: term_variants_pred.cases)


[STATEMENT]
lemma (in bounded_lattice_bot) atomic_implies_join_prime:
  assumes "atomic x"
  shows "join_irreducible x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. join_irreducible x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
atomic x

goal (1 subgoal):
 1. join_irreducible x
[PROOF STEP]
unfolding
    atomic_def
    join_irreducible_def'
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom> \<and> (\<forall>y\<le>x. y = \<bottom> \<or> y = x)

goal (1 subgoal):
 1. x \<noteq> \<bottom> \<and> (\<forall>y z. x = y \<squnion> z \<longrightarrow> x = y \<or> x = z)
[PROOF STEP]
by (metis (no_types, opaque_lifting)
        sup.cobounded2
        sup_bot.right_neutral)


[STATEMENT]
lemma weak_reflection_of_barbs_and_set_of_barbs:
  fixes Rel :: "('proc \<times> 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  shows "rel_weakly_reflects_barbs Rel CWB = (\<forall>Barbs. rel_weakly_reflects_barb_set Rel CWB Barbs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_weakly_reflects_barbs Rel CWB = (\<forall>Barbs. rel_weakly_reflects_barb_set Rel CWB Barbs)
[PROOF STEP]
by blast


[STATEMENT]
lemma fresh_Some:
  shows "a \<sharp> Some x \<longleftrightarrow> a \<sharp> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> Some x = a \<sharp> x
[PROOF STEP]
by (simp add: fresh_def supp_Some)


[STATEMENT]
lemma permute_flip_at:
  fixes a b c::"'a::at"
  shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)
[PROOF STEP]
unfolding flip_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (atom a \<rightleftharpoons> atom b) \<bullet> c = (if c = a then b else if c = b then a else c)
[PROOF STEP]
apply (rule atom_eq_iff [THEN iffD1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom ((atom a \<rightleftharpoons> atom b) \<bullet> c) = atom (if c = a then b else if c = b then a else c)
[PROOF STEP]
apply (subst atom_eqvt [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (atom a \<rightleftharpoons> atom b) \<bullet> atom c = atom (if c = a then b else if c = b then a else c)
[PROOF STEP]
apply (simp add: swap_atom)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_minimal_basis_trd_distinct:
  assumes min: "is_minimal_basis (set (x # xs))" and dist: "distinct (x # xs)"
  shows "distinct ((trd xs x) # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
let ?y = "trd xs x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
from min
[PROOF STATE]
proof (chain)
picking this:
is_minimal_basis (set (x # xs))
[PROOF STEP]
have lty: "lt ?y = lt x"
[PROOF STATE]
proof (prove)
using this:
is_minimal_basis (set (x # xs))

goal (1 subgoal):
 1. lt (trd xs x) = lt x
[PROOF STEP]
proof (rule minimal_basis_red_rtrancl_lt, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (red (set (x # xs) - {x}))\<^sup>*\<^sup>* x (trd xs x)
[PROOF STEP]
from dist
[PROOF STATE]
proof (chain)
picking this:
distinct (x # xs)
[PROOF STEP]
have "x \<notin> set xs"
[PROOF STATE]
proof (prove)
using this:
distinct (x # xs)

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

goal (1 subgoal):
 1. (red (set (x # xs) - {x}))\<^sup>*\<^sup>* x (trd xs x)
[PROOF STEP]
hence eq: "set (x # xs) - {x} = set xs"
[PROOF STATE]
proof (prove)
using this:
x \<notin> set xs

goal (1 subgoal):
 1. set (x # xs) - {x} = set xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (x # xs) - {x} = set xs

goal (1 subgoal):
 1. (red (set (x # xs) - {x}))\<^sup>*\<^sup>* x (trd xs x)
[PROOF STEP]
show "(red (set (x # xs) - {x}))\<^sup>*\<^sup>* x (trd xs x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (red (set (x # xs) - {x}))\<^sup>*\<^sup>* x (trd xs x)
[PROOF STEP]
unfolding eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (red (set xs))\<^sup>*\<^sup>* x (trd xs x)
[PROOF STEP]
by (rule trd_red_rtrancl)
[PROOF STATE]
proof (state)
this:
(red (set (x # xs) - {x}))\<^sup>*\<^sup>* x (trd xs x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lt (trd xs x) = lt x

goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
have "?y \<notin> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trd xs x \<notin> set xs
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trd xs x \<in> set xs \<Longrightarrow> False
[PROOF STEP]
assume "?y \<in> set xs"
[PROOF STATE]
proof (state)
this:
trd xs x \<in> set xs

goal (1 subgoal):
 1. trd xs x \<in> set xs \<Longrightarrow> False
[PROOF STEP]
hence "?y \<in> set (x # xs)"
[PROOF STATE]
proof (prove)
using this:
trd xs x \<in> set xs

goal (1 subgoal):
 1. trd xs x \<in> set (x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
trd xs x \<in> set (x # xs)

goal (1 subgoal):
 1. trd xs x \<in> set xs \<Longrightarrow> False
[PROOF STEP]
with min
[PROOF STATE]
proof (chain)
picking this:
is_minimal_basis (set (x # xs))
trd xs x \<in> set (x # xs)
[PROOF STEP]
have "\<not> lt ?y adds\<^sub>t lt x"
[PROOF STATE]
proof (prove)
using this:
is_minimal_basis (set (x # xs))
trd xs x \<in> set (x # xs)

goal (1 subgoal):
 1. \<not> lt (trd xs x) adds\<^sub>t lt x
[PROOF STEP]
proof (rule is_minimal_basisD2, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trd xs x \<noteq> x
[PROOF STEP]
show "?y \<noteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trd xs x \<noteq> x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trd xs x = x \<Longrightarrow> False
[PROOF STEP]
assume "?y = x"
[PROOF STATE]
proof (state)
this:
trd xs x = x

goal (1 subgoal):
 1. trd xs x = x \<Longrightarrow> False
[PROOF STEP]
from dist
[PROOF STATE]
proof (chain)
picking this:
distinct (x # xs)
[PROOF STEP]
have "x \<notin> set xs"
[PROOF STATE]
proof (prove)
using this:
distinct (x # xs)

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

goal (1 subgoal):
 1. trd xs x = x \<Longrightarrow> False
[PROOF STEP]
with \<open>?y \<in> set xs\<close>
[PROOF STATE]
proof (chain)
picking this:
trd xs x \<in> set xs
x \<notin> set xs
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
trd xs x \<in> set xs
x \<notin> set xs

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding \<open>?y = x\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> set xs
x \<notin> set xs

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trd xs x \<noteq> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> lt (trd xs x) adds\<^sub>t lt x

goal (1 subgoal):
 1. trd xs x \<in> set xs \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
\<not> lt (trd xs x) adds\<^sub>t lt x

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding lty
[PROOF STATE]
proof (prove)
using this:
\<not> lt x adds\<^sub>t lt x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trd xs x \<notin> set xs

goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
trd xs x \<notin> set xs

goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
from dist
[PROOF STATE]
proof (chain)
picking this:
distinct (x # xs)
[PROOF STEP]
have "distinct xs"
[PROOF STATE]
proof (prove)
using this:
distinct (x # xs)

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

goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
trd xs x \<notin> set xs
distinct xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trd xs x \<notin> set xs
distinct xs

goal (1 subgoal):
 1. distinct (trd xs x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (trd xs x # xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lfinite_lappend [simp]:
  "lfinite (lappend xs ys) \<longleftrightarrow> lfinite xs \<and> lfinite ys"
  (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfinite (lappend xs ys) = (lfinite xs \<and> lfinite ys)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lfinite (lappend xs ys) \<Longrightarrow> lfinite xs \<and> lfinite ys
 2. lfinite xs \<and> lfinite ys \<Longrightarrow> lfinite (lappend xs ys)
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
lfinite (lappend xs ys)

goal (2 subgoals):
 1. lfinite (lappend xs ys) \<Longrightarrow> lfinite xs \<and> lfinite ys
 2. lfinite xs \<and> lfinite ys \<Longrightarrow> lfinite (lappend xs ys)
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
lfinite (lappend xs ys)

goal (1 subgoal):
 1. lfinite xs \<and> lfinite ys
[PROOF STEP]
proof(induct zs\<equiv>"lappend xs ys" arbitrary: xs ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs ys. LNil = lappend xs ys \<Longrightarrow> lfinite xs \<and> lfinite ys
 2. \<And>xs x xsa ys. \<lbrakk>lfinite xs; \<And>xsa ys. xs = lappend xsa ys \<Longrightarrow> lfinite xsa \<and> lfinite ys; LCons x xs = lappend xsa ys\<rbrakk> \<Longrightarrow> lfinite xsa \<and> lfinite ys
[PROOF STEP]
case lfinite_LNil
[PROOF STATE]
proof (state)
this:
LNil = lappend xs ys

goal (2 subgoals):
 1. \<And>xs ys. LNil = lappend xs ys \<Longrightarrow> lfinite xs \<and> lfinite ys
 2. \<And>xs x xsa ys. \<lbrakk>lfinite xs; \<And>xsa ys. xs = lappend xsa ys \<Longrightarrow> lfinite xsa \<and> lfinite ys; LCons x xs = lappend xsa ys\<rbrakk> \<Longrightarrow> lfinite xsa \<and> lfinite ys
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
LNil = lappend xs ys

goal (1 subgoal):
 1. lfinite xs \<and> lfinite ys
[PROOF STEP]
by(simp add: LNil_eq_lappend_iff)
[PROOF STATE]
proof (state)
this:
lfinite xs \<and> lfinite ys

goal (1 subgoal):
 1. \<And>xs x xsa ys. \<lbrakk>lfinite xs; \<And>xsa ys. xs = lappend xsa ys \<Longrightarrow> lfinite xsa \<and> lfinite ys; LCons x xs = lappend xsa ys\<rbrakk> \<Longrightarrow> lfinite xsa \<and> lfinite ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs x xsa ys. \<lbrakk>lfinite xs; \<And>xsa ys. xs = lappend xsa ys \<Longrightarrow> lfinite xsa \<and> lfinite ys; LCons x xs = lappend xsa ys\<rbrakk> \<Longrightarrow> lfinite xsa \<and> lfinite ys
[PROOF STEP]
case (lfinite_LConsI zs z)
[PROOF STATE]
proof (state)
this:
lfinite zs
zs = lappend ?xs ?ys \<Longrightarrow> lfinite ?xs \<and> lfinite ?ys
LCons z zs = lappend xs ys

goal (1 subgoal):
 1. \<And>xs x xsa ys. \<lbrakk>lfinite xs; \<And>xsa ys. xs = lappend xsa ys \<Longrightarrow> lfinite xsa \<and> lfinite ys; LCons x xs = lappend xsa ys\<rbrakk> \<Longrightarrow> lfinite xsa \<and> lfinite ys
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
lfinite zs
zs = lappend ?xs ?ys \<Longrightarrow> lfinite ?xs \<and> lfinite ?ys
LCons z zs = lappend xs ys

goal (1 subgoal):
 1. lfinite xs \<and> lfinite ys
[PROOF STEP]
by(cases xs)(cases ys, simp_all)
[PROOF STATE]
proof (state)
this:
lfinite xs \<and> lfinite ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lfinite xs \<and> lfinite ys

goal (1 subgoal):
 1. lfinite xs \<and> lfinite ys \<Longrightarrow> lfinite (lappend xs ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lfinite xs \<and> lfinite ys \<Longrightarrow> lfinite (lappend xs ys)
[PROOF STEP]
assume ?rhs (is "?xs \<and> ?ys")
[PROOF STATE]
proof (state)
this:
lfinite xs \<and> lfinite ys

goal (1 subgoal):
 1. lfinite xs \<and> lfinite ys \<Longrightarrow> lfinite (lappend xs ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lfinite xs \<and> lfinite ys
[PROOF STEP]
obtain ?xs ?ys
[PROOF STATE]
proof (prove)
using this:
lfinite xs \<and> lfinite ys

goal (1 subgoal):
 1. (\<lbrakk>lfinite xs; lfinite ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
lfinite xs
lfinite ys

goal (1 subgoal):
 1. lfinite xs \<and> lfinite ys \<Longrightarrow> lfinite (lappend xs ys)
[PROOF STEP]
thus ?lhs
[PROOF STATE]
proof (prove)
using this:
lfinite xs
lfinite ys

goal (1 subgoal):
 1. lfinite (lappend xs ys)
[PROOF STEP]
by induct simp_all
[PROOF STATE]
proof (state)
this:
lfinite (lappend xs ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ltake_plus_conv_lappend:
  "ltake (n + m) xs = lappend (ltake n xs) (ltake m (ldrop n xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltake (n + m) xs = lappend (ltake n xs) (ltake m (ldrop n xs))
[PROOF STEP]
by(coinduction arbitrary: n m xs rule: llist.coinduct_strong)(auto intro!: exI simp add: iadd_is_0 ltl_ltake epred_iadd1 ldrop_ltl)


[STATEMENT]
lemma ltl_ltakeWhile:
  "ltl (ltakeWhile P xs) = (if P (lhd xs) then ltakeWhile P (ltl xs) else LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltl (ltakeWhile P xs) = (if P (lhd xs) then ltakeWhile P (ltl xs) else LNil)
[PROOF STEP]
by(cases xs) simp_all


[STATEMENT]
lemma lift_subst_ML:
 "lift k (subst\<^sub>M\<^sub>L \<sigma> v) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift k (subst\<^sub>M\<^sub>L \<sigma> v) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k v)
[PROOF STEP]
apply(induct \<sigma> v rule:subst_ML.induct)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>\<sigma> nm. lift k (subst\<^sub>M\<^sub>L \<sigma> (C\<^sub>M\<^sub>L nm)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (C\<^sub>M\<^sub>L nm))
 2. \<And>\<sigma> X. lift k (subst\<^sub>M\<^sub>L \<sigma> (V\<^sub>M\<^sub>L X)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (V\<^sub>M\<^sub>L X))
 3. \<And>\<sigma> v vs. \<lbrakk>lift k (subst\<^sub>M\<^sub>L \<sigma> v) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k v); \<And>x. x \<in> set vs \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> x) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k x)\<rbrakk> \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> (A\<^sub>M\<^sub>L v vs)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (A\<^sub>M\<^sub>L v vs))
 4. \<And>\<sigma> v. lift k (subst\<^sub>M\<^sub>L (V\<^sub>M\<^sub>L 0 ## \<sigma>) v) = subst\<^sub>M\<^sub>L (lift k \<circ> V\<^sub>M\<^sub>L 0 ## \<sigma>) (lift k v) \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> (Lam\<^sub>M\<^sub>L v)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (Lam\<^sub>M\<^sub>L v))
 5. \<And>\<sigma> nm vs. (\<And>x. x \<in> set vs \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> x) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k x)) \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> (C\<^sub>U nm vs)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (C\<^sub>U nm vs))
 6. \<And>\<sigma> x vs. (\<And>xa. xa \<in> set vs \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> xa) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k xa)) \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> (V\<^sub>U x vs)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (V\<^sub>U x vs))
 7. \<And>\<sigma> v vs n. \<lbrakk>lift k (subst\<^sub>M\<^sub>L \<sigma> v) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k v); \<And>x. x \<in> set vs \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> x) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k x)\<rbrakk> \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> (Clo v vs n)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (Clo v vs n))
 8. \<And>\<sigma> u v. \<lbrakk>lift k (subst\<^sub>M\<^sub>L \<sigma> u) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k u); lift k (subst\<^sub>M\<^sub>L \<sigma> v) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k v)\<rbrakk> \<Longrightarrow> lift k (subst\<^sub>M\<^sub>L \<sigma> (apply u v)) = subst\<^sub>M\<^sub>L (lift k \<circ> \<sigma>) (lift k (apply u v))
[PROOF STEP]
apply(simp_all add: o_assoc lift_o_shift del:apply_cons_ML)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> v. lift k (subst\<^sub>M\<^sub>L (V\<^sub>M\<^sub>L 0 ## \<sigma>) v) = subst\<^sub>M\<^sub>L (V\<^sub>M\<^sub>L 0 ## (lift k \<circ> \<sigma>)) (lift k v) \<Longrightarrow> subst\<^sub>M\<^sub>L (V\<^sub>M\<^sub>L 0 ## (lift k \<circ> \<sigma>)) (lift k v) = subst\<^sub>M\<^sub>L (V\<^sub>M\<^sub>L 0 ## (\<lambda>a. lift k (\<sigma> a))) (lift k v)
[PROOF STEP]
apply(simp add:o_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem normal_intersection_quotient_isom:
  shows "(\<lambda>X. the_elem ((\<lambda>g. H #> g) ` X)) \<in> iso ((G\<lparr>carrier := S\<rparr>) Mod (H \<inter> S)) (((G\<lparr>carrier := H <#> S\<rparr>)) Mod H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>X. the_elem ((#>) H ` X)) \<in> Group.iso (G\<lparr>carrier := S\<rparr> Mod H \<inter> S) (G\<lparr>carrier := H <#> S\<rparr> Mod H)
[PROOF STEP]
using normal_intersection_hom_kernel[symmetric] normal_intersection_hom normal_intersection_hom_surj
[PROOF STATE]
proof (prove)
using this:
H \<inter> S = kernel (G\<lparr>carrier := S\<rparr>) (G\<lparr>carrier := H <#> S\<rparr> Mod H) ((#>) H)
group_hom (G\<lparr>carrier := S\<rparr>) (G\<lparr>carrier := H <#> S\<rparr> Mod H) ((#>) H)
(#>) H ` carrier (G\<lparr>carrier := S\<rparr>) = carrier (G\<lparr>carrier := H <#> S\<rparr> Mod H)

goal (1 subgoal):
 1. (\<lambda>X. the_elem ((#>) H ` X)) \<in> Group.iso (G\<lparr>carrier := S\<rparr> Mod H \<inter> S) (G\<lparr>carrier := H <#> S\<rparr> Mod H)
[PROOF STEP]
by (metis group_hom.FactGroup_iso_set)


[STATEMENT]
lemma s_gt_0: "s > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < s
[PROOF STEP]
using \<epsilon>_range
[PROOF STATE]
proof (prove)
using this:
\<epsilon> \<in> {0<..<1}

goal (1 subgoal):
 1. 0 < s
[PROOF STEP]
by (simp add:s_def)


[STATEMENT]
lemma iarray_to_matrix_matrix_to_iarray:
  fixes A::"'a^'columns::{mod_type}^'rows::{mod_type}"
  shows "iarray_to_matrix (matrix_to_iarray A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iarray_to_matrix (matrix_to_iarray A) = A
[PROOF STEP]
unfolding matrix_to_iarray_def iarray_to_matrix_def o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i j. IArray (map (\<lambda>x. vec_to_iarray (A $ mod_type_class.from_nat x)) [0..<CARD('rows)]) !! mod_type_class.to_nat i !! mod_type_class.to_nat j) = A
[PROOF STEP]
by (vector, auto, metis IArray.sub_def vec_to_iarray_nth')


[STATEMENT]
lemma (in is_functor) cf_umap_of_cf_hom_commute:
  assumes "category \<alpha> \<AA>"
    and "category \<alpha> \<BB>"
    and "c \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
    and "r \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
    and "u : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>"
    and "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
  shows
    "umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> =
      cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a"
  (is \<open>?uof_b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?rf = ?cf \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?uof_a\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> = cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> = cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a
[PROOF STEP]
from is_functor_axioms category_cat_Set assms(1,2,4-6)
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
category \<alpha> (cat_Set \<alpha>)
category \<alpha> \<AA>
category \<alpha> \<BB>
r \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
u : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
have b_rf:
    "?uof_b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?rf : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
category \<alpha> (cat_Set \<alpha>)
category \<alpha> \<AA>
category \<alpha> \<BB>
r \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
u : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
      )
[PROOF STATE]
proof (state)
this:
umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> = cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a
[PROOF STEP]
from is_functor_axioms category_cat_Set assms(1,2,4-6)
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
category \<alpha> (cat_Set \<alpha>)
category \<alpha> \<AA>
category \<alpha> \<BB>
r \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
u : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
have cf_a:
    "?cf \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?uof_a : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
category \<alpha> (cat_Set \<alpha>)
category \<alpha> \<AA>
category \<alpha> \<BB>
r \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
u : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
by (cs_concl cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros)
[PROOF STATE]
proof (state)
this:
cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> = cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> = cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a
[PROOF STEP]
proof(rule arr_Set_eqI[of \<alpha>])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. arr_Set \<alpha> (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)
 2. arr_Set \<alpha> (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)
 3. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>
 4. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrDom\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrDom\<rparr>
 5. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrCod\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrCod\<rparr>
[PROOF STEP]
from b_rf
[PROOF STATE]
proof (chain)
picking this:
umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
show arr_Set_b_rf: "arr_Set \<alpha> (?uof_b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?rf)"
[PROOF STATE]
proof (prove)
using this:
umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. arr_Set \<alpha> (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)
[PROOF STEP]
by (auto dest: cat_Set_is_arrD(1))
[PROOF STATE]
proof (state)
this:
arr_Set \<alpha> (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)

goal (4 subgoals):
 1. arr_Set \<alpha> (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)
 2. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>
 3. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrDom\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrDom\<rparr>
 4. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrCod\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrCod\<rparr>
[PROOF STEP]
from b_rf
[PROOF STATE]
proof (chain)
picking this:
umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
have dom_lhs:
      "\<D>\<^sub>\<circ> ((?uof_b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?rf)\<lparr>ArrVal\<rparr>) = Hom \<AA> r a"
[PROOF STATE]
proof (prove)
using this:
umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>) = Hom \<AA> r a
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_cs_simps)+
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>) = Hom \<AA> r a

goal (4 subgoals):
 1. arr_Set \<alpha> (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)
 2. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>
 3. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrDom\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrDom\<rparr>
 4. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrCod\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrCod\<rparr>
[PROOF STEP]
from cf_a
[PROOF STATE]
proof (chain)
picking this:
cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
show arr_Set_cf_a: "arr_Set \<alpha> (?cf \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?uof_a)"
[PROOF STATE]
proof (prove)
using this:
cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. arr_Set \<alpha> (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)
[PROOF STEP]
by (auto dest: cat_Set_is_arrD(1))
[PROOF STATE]
proof (state)
this:
arr_Set \<alpha> (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)

goal (3 subgoals):
 1. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>
 2. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrDom\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrDom\<rparr>
 3. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrCod\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrCod\<rparr>
[PROOF STEP]
from cf_a
[PROOF STATE]
proof (chain)
picking this:
cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
have dom_rhs:
      "\<D>\<^sub>\<circ> ((?cf \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?uof_a)\<lparr>ArrVal\<rparr>) = Hom \<AA> r a"
[PROOF STATE]
proof (prove)
using this:
cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>) = Hom \<AA> r a
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>) = Hom \<AA> r a

goal (3 subgoals):
 1. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>
 2. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrDom\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrDom\<rparr>
 3. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrCod\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrCod\<rparr>
[PROOF STEP]
show "(?uof_b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?rf)\<lparr>ArrVal\<rparr> = (?cf \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?uof_a)\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>)
 2. vsv ((cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>)
 3. Hom \<AA> r a = Hom \<AA> r a
 4. \<And>aa. aa : r \<mapsto>\<^bsub>\<AA>\<^esub> a \<Longrightarrow> (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>\<lparr>aa\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>\<lparr>aa\<rparr>
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>)
 2. vsv ((cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>)
 3. Hom \<AA> r a = Hom \<AA> r a
 4. \<And>aa. aa : r \<mapsto>\<^bsub>\<AA>\<^esub> a \<Longrightarrow> (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>\<lparr>aa\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>\<lparr>aa\<rparr>
[PROOF STEP]
assume "q : r \<mapsto>\<^bsub>\<AA>\<^esub> a"
[PROOF STATE]
proof (state)
this:
q : r \<mapsto>\<^bsub>\<AA>\<^esub> a

goal (4 subgoals):
 1. vsv ((umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>)
 2. vsv ((cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>)
 3. Hom \<AA> r a = Hom \<AA> r a
 4. \<And>aa. aa : r \<mapsto>\<^bsub>\<AA>\<^esub> a \<Longrightarrow> (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>\<lparr>aa\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>\<lparr>aa\<rparr>
[PROOF STEP]
with is_functor_axioms category_cat_Set assms
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
category \<alpha> (cat_Set \<alpha>)
category \<alpha> \<AA>
category \<alpha> \<BB>
c \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
r \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
u : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
q : r \<mapsto>\<^bsub>\<AA>\<^esub> a
[PROOF STEP]
show
        "(?uof_b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?rf)\<lparr>ArrVal\<rparr>\<lparr>q\<rparr> =
          (?cf \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?uof_a)\<lparr>ArrVal\<rparr>\<lparr>q\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
category \<alpha> (cat_Set \<alpha>)
category \<alpha> \<AA>
category \<alpha> \<BB>
c \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
r \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
u : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
q : r \<mapsto>\<^bsub>\<AA>\<^esub> a

goal (1 subgoal):
 1. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>\<lparr>q\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>\<lparr>q\<rparr>
[PROOF STEP]
by
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cat_op_simps
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
         )
[PROOF STATE]
proof (state)
this:
(umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>\<lparr>q\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>\<lparr>q\<rparr>

goal (3 subgoals):
 1. vsv ((umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>)
 2. vsv ((cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>)
 3. Hom \<AA> r a = Hom \<AA> r a
[PROOF STEP]
qed (use arr_Set_b_rf arr_Set_cf_a in auto)
[PROOF STATE]
proof (state)
this:
(umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>

goal (2 subgoals):
 1. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrDom\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrDom\<rparr>
 2. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrCod\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrCod\<rparr>
[PROOF STEP]
qed (use b_rf cf_a in \<open>cs_concl cs_shallow cs_simp: cat_cs_simps\<close>)+
[PROOF STATE]
proof (state)
this:
umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> = cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma next_execs_subset:
shows "\<forall>s execs u . actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
fix s execs u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
have "actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
unfolding Kernel.next_execs_def actions_in_execution_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. \<exists>aseq\<in>set ((execs(current s := fst (snd (CISK_control s (current s) (execs (current s)))))) u). a \<in> set aseq} \<subseteq> {a. \<exists>aseq\<in>set (execs u). a \<in> set aseq}
[PROOF STEP]
by (cases "(s,(current s),execs (current s))" rule: CISK_control.cases,auto split: if_split_asm)
[PROOF STATE]
proof (state)
this:
actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)

goal (1 subgoal):
 1. \<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
actions_in_execution (next_execs ?s2 ?execs2 ?u2) \<subseteq> actions_in_execution (?execs2 ?u2)

goal (1 subgoal):
 1. \<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
actions_in_execution (next_execs ?s2 ?execs2 ?u2) \<subseteq> actions_in_execution (?execs2 ?u2)

goal (1 subgoal):
 1. \<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma irreducible\<^sub>d_mI:
  assumes f0: "degree_m f > 0"
      and main: "\<And>g h. Mp g = g \<Longrightarrow> Mp h = h \<Longrightarrow> degree g > 0 \<Longrightarrow> degree g < degree_m f \<Longrightarrow> degree h > 0 \<Longrightarrow> degree h < degree_m f \<Longrightarrow> f =m g * h \<Longrightarrow> False"
    shows "irreducible\<^sub>d_m f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreducible\<^sub>d_m f
[PROOF STEP]
proof (unfold irreducible\<^sub>d_m_def, intro conjI allI impI f0 notI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g h. \<lbrakk>degree_m g < degree_m f; degree_m h < degree_m f; f =m g * h\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix g h
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g h. \<lbrakk>degree_m g < degree_m f; degree_m h < degree_m f; f =m g * h\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume deg: "degree_m g < degree_m f" "degree_m h < degree_m f" and "f =m g * h"
[PROOF STATE]
proof (state)
this:
degree_m g < degree_m f
degree_m h < degree_m f
f =m g * h

goal (1 subgoal):
 1. \<And>g h. \<lbrakk>degree_m g < degree_m f; degree_m h < degree_m f; f =m g * h\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
degree_m g < degree_m f
degree_m h < degree_m f
f =m g * h
[PROOF STEP]
have f: "f =m Mp g * Mp h"
[PROOF STATE]
proof (prove)
using this:
degree_m g < degree_m f
degree_m h < degree_m f
f =m g * h

goal (1 subgoal):
 1. f =m Mp g * Mp h
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f =m Mp g * Mp h

goal (1 subgoal):
 1. \<And>g h. \<lbrakk>degree_m g < degree_m f; degree_m h < degree_m f; f =m g * h\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "degree_m f \<le> degree_m g + degree_m h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree_m f \<le> degree_m g + degree_m h
[PROOF STEP]
unfolding f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree_m (Mp g * Mp h) \<le> degree_m g + degree_m h
[PROOF STEP]
using degree_mult_le order.trans
[PROOF STATE]
proof (prove)
using this:
degree (?p * ?q) \<le> degree ?p + degree ?q
\<lbrakk>?a \<le> ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a \<le> ?c

goal (1 subgoal):
 1. degree_m (Mp g * Mp h) \<le> degree_m g + degree_m h
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
degree_m f \<le> degree_m g + degree_m h

goal (1 subgoal):
 1. \<And>g h. \<lbrakk>degree_m g < degree_m f; degree_m h < degree_m f; f =m g * h\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with main[of "Mp g" "Mp h"] deg f
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Mp g =m g; Mp h =m h; 0 < degree_m g; degree_m g < degree_m f; 0 < degree_m h; degree_m h < degree_m f; f =m Mp g * Mp h\<rbrakk> \<Longrightarrow> False
degree_m g < degree_m f
degree_m h < degree_m f
f =m Mp g * Mp h
degree_m f \<le> degree_m g + degree_m h
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Mp g =m g; Mp h =m h; 0 < degree_m g; degree_m g < degree_m f; 0 < degree_m h; degree_m h < degree_m f; f =m Mp g * Mp h\<rbrakk> \<Longrightarrow> False
degree_m g < degree_m f
degree_m h < degree_m f
f =m Mp g * Mp h
degree_m f \<le> degree_m g + degree_m h

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in igb_fr_graph) find_lasso_correct: "find_lasso \<le> find_lasso_spec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_lasso \<le> find_lasso_spec
[PROOF STEP]
unfolding find_lasso_spec_def find_lasso_def find_ce_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> is_lasso_prpl prpl | Some (x, xa) \<Rightarrow> ce_correct x xa) \<bind> (\<lambda>ce. case ce of None \<Rightarrow> RETURN None | Some (Vr, Vl) \<Rightarrow> reconstruct_lasso Vr Vl \<bind> (\<lambda>l. RETURN (Some l))) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> is_lasso_prpl prpl | Some x \<Rightarrow> is_lasso_prpl x)
[PROOF STEP]
apply (refine_rcg refine_vcg order_trans[OF reconstruct_lasso_correct])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>case x of None \<Rightarrow> \<forall>prpl. \<not> is_lasso_prpl prpl | Some (x, xa) \<Rightarrow> ce_correct x xa; x = None\<rbrakk> \<Longrightarrow> case None of None \<Rightarrow> \<forall>prpl. \<not> is_lasso_prpl prpl | Some x \<Rightarrow> is_lasso_prpl x
 2. \<And>x xa a b. \<lbrakk>case x of None \<Rightarrow> \<forall>prpl. \<not> is_lasso_prpl prpl | Some (x, xa) \<Rightarrow> ce_correct x xa; x = Some xa; xa = (a, b)\<rbrakk> \<Longrightarrow> ce_correct a b
 3. \<And>x xa a b xb. \<lbrakk>case x of None \<Rightarrow> \<forall>prpl. \<not> is_lasso_prpl prpl | Some (x, xa) \<Rightarrow> ce_correct x xa; x = Some xa; xa = (a, b); is_lasso_prpl xb\<rbrakk> \<Longrightarrow> case Some xb of None \<Rightarrow> \<forall>prpl. \<not> is_lasso_prpl prpl | Some x \<Rightarrow> is_lasso_prpl x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma radical_dvd [simp, intro]: "radical x dvd x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. radical x dvd x
[PROOF STEP]
by (cases "x = 0") (force intro: prime_factorization_subset_imp_dvd mset_set_set_mset_msubset)+


[STATEMENT]
lemma ThrowRedsNull:
  "P \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle> \<Longrightarrow> P \<turnstile> \<langle>throw e,s\<rangle> \<rightarrow>* \<langle>THROW NullPointer,s'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle> \<Longrightarrow> P \<turnstile> \<langle>throw e,s\<rangle> \<rightarrow>* \<langle>THROW NullPointer,s'\<rangle>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle> \<Longrightarrow> P \<turnstile> \<langle>throw e,s\<rangle> \<rightarrow>* \<langle>THROW NullPointer,s'\<rangle>
[PROOF STEP]
by(rule ThrowReds[THEN rtrancl_into_rtrancl, OF _ RedThrowNull])


[STATEMENT]
lemma msetext_huet_compat_snoc: "msetext_huet gt ys xs \<Longrightarrow> msetext_huet gt (ys @ [x]) (xs @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msetext_huet gt ys xs \<Longrightarrow> msetext_huet gt (ys @ [x]) (xs @ [x])
[PROOF STEP]
unfolding msetext_huet_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset xs \<noteq> mset ys \<and> (\<forall>x. count (mset ys) x < count (mset xs) x \<longrightarrow> (\<exists>y. gt y x \<and> count (mset xs) y < count (mset ys) y)) \<Longrightarrow> mset (xs @ [x]) \<noteq> mset (ys @ [x]) \<and> (\<forall>xa. count (mset (ys @ [x])) xa < count (mset (xs @ [x])) xa \<longrightarrow> (\<exists>y. gt y xa \<and> count (mset (xs @ [x])) y < count (mset (ys @ [x])) y))
[PROOF STEP]
by auto


[STATEMENT]
lemma powr_at_top_neg:
  assumes "(a::real) > 0" "a < 1"
  shows   "((\<lambda>x. a powr x) \<longlongrightarrow> 0) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_top
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_top
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < a
a < 1
[PROOF STEP]
have "LIM x at_top. ln (inverse a) * x :> at_top"
[PROOF STATE]
proof (prove)
using this:
0 < a
a < 1

goal (1 subgoal):
 1. filterlim ((*) (ln (inverse a))) at_top at_top
[PROOF STEP]
by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const])
       (simp_all add: filterlim_ident field_simps)
[PROOF STATE]
proof (state)
this:
filterlim ((*) (ln (inverse a))) at_top at_top

goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_top
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < a
a < 1
filterlim ((*) (ln (inverse a))) at_top at_top
[PROOF STEP]
have "LIM x at_top. ln a * x :> at_bot"
[PROOF STATE]
proof (prove)
using this:
0 < a
a < 1
filterlim ((*) (ln (inverse a))) at_top at_top

goal (1 subgoal):
 1. filterlim ((*) (ln a)) at_bot at_top
[PROOF STEP]
by (subst filterlim_uminus_at_bot) (simp add: ln_inverse)
[PROOF STATE]
proof (state)
this:
filterlim ((*) (ln a)) at_bot at_top

goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_top
[PROOF STEP]
hence "((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_top"
[PROOF STATE]
proof (prove)
using this:
filterlim ((*) (ln a)) at_bot at_top

goal (1 subgoal):
 1. ((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_top
[PROOF STEP]
by (intro filterlim_compose[OF exp_at_bot]) (simp_all add: mult.commute)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_top

goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_top
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < a
a < 1
((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < a
a < 1
((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_top

goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_top
[PROOF STEP]
unfolding powr_def
[PROOF STATE]
proof (prove)
using this:
0 < a
a < 1
((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_top

goal (1 subgoal):
 1. ((\<lambda>x. if a = 0 then 0 else exp (x * ln a)) \<longlongrightarrow> 0) at_top
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((powr) a \<longlongrightarrow> 0) at_top

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma glist_insert_dj_id_impl:
    "\<lbrakk> x\<notin>s; (l,s)\<in>br set distinct \<rbrakk> \<Longrightarrow> (x#l,insert x s)\<in>br set distinct"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> s; (l, s) \<in> br set distinct\<rbrakk> \<Longrightarrow> (x # l, insert x s) \<in> br set distinct
[PROOF STEP]
by (auto simp: br_def)


[STATEMENT]
lemma IIA_swf: "IIA(swf f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IIA (swf f)
[PROOF STEP]
proof(clarsimp simp: IIA_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
fix P P' a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
assume "P:Prof" "P':Prof" and iff: "\<forall>i. ((a,b) \<in> P i) = ((a,b) \<in> P' i)"
[PROOF STATE]
proof (state)
this:
P \<in> Prof
P' \<in> Prof
\<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)

goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
hence [simp]: "!!i x. (x,x) ~: P i \<and> (x,x) ~: P' i"
[PROOF STATE]
proof (prove)
using this:
P \<in> Prof
P' \<in> Prof
\<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)

goal (1 subgoal):
 1. \<And>i x. (x, x) \<notin> P i \<and> (x, x) \<notin> P' i
[PROOF STEP]
by(simp add:Prof_def Pi_def slo_defs)
[PROOF STATE]
proof (state)
this:
(?x, ?x) \<notin> P ?i \<and> (?x, ?x) \<notin> P' ?i

goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
have iff':  "a\<noteq>b \<longrightarrow> (\<forall>i. ((b,a) \<in> P i) = ((b,a) \<in> P' i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> b \<longrightarrow> (\<forall>i. (b <\<^bsub>P i\<^esub> a) = (b <\<^bsub>P' i\<^esub> a))
[PROOF STEP]
using iff \<open>P:Prof\<close> \<open>P':Prof\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)
P \<in> Prof
P' \<in> Prof

goal (1 subgoal):
 1. a \<noteq> b \<longrightarrow> (\<forall>i. (b <\<^bsub>P i\<^esub> a) = (b <\<^bsub>P' i\<^esub> a))
[PROOF STEP]
unfolding Prof_def Pi_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)
P \<in> {f. \<forall>x. x \<in> I \<longrightarrow> f x \<in> Lin}
P' \<in> {f. \<forall>x. x \<in> I \<longrightarrow> f x \<in> Lin}

goal (1 subgoal):
 1. a \<noteq> b \<longrightarrow> (\<forall>i. (b <\<^bsub>P i\<^esub> a) = (b <\<^bsub>P' i\<^esub> a))
[PROOF STEP]
by simp (metis iff notin_Lin_iff)
[PROOF STATE]
proof (state)
this:
a \<noteq> b \<longrightarrow> (\<forall>i. (b <\<^bsub>P i\<^esub> a) = (b <\<^bsub>P' i\<^esub> a))

goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
let ?abP = "Top {a,b} o P"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
let ?abP' = "Top {a,b} o P'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
have "\<forall>i c. (c, f ?abP) : ?abP i \<longrightarrow> (c, f ?abP) : ?abP' i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i c. c <\<^bsub>(Top {a, b} \<circ> P) i\<^esub> f (Top {a, b} \<circ> P) \<longrightarrow> c <\<^bsub>(Top {a, b} \<circ> P') i\<^esub> f (Top {a, b} \<circ> P)
[PROOF STEP]
using una_Top[of P "{a,b}", OF \<open>P:Prof\<close>] iff iff'
[PROOF STATE]
proof (prove)
using this:
{a, b} \<noteq> {} \<Longrightarrow> f (Top {a, b} \<circ> P) \<in> {a, b}
\<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)
a \<noteq> b \<longrightarrow> (\<forall>i. (b <\<^bsub>P i\<^esub> a) = (b <\<^bsub>P' i\<^esub> a))

goal (1 subgoal):
 1. \<forall>i c. c <\<^bsub>(Top {a, b} \<circ> P) i\<^esub> f (Top {a, b} \<circ> P) \<longrightarrow> c <\<^bsub>(Top {a, b} \<circ> P') i\<^esub> f (Top {a, b} \<circ> P)
[PROOF STEP]
by(auto simp add:Top_def)
[PROOF STATE]
proof (state)
this:
\<forall>i c. c <\<^bsub>(Top {a, b} \<circ> P) i\<^esub> f (Top {a, b} \<circ> P) \<longrightarrow> c <\<^bsub>(Top {a, b} \<circ> P') i\<^esub> f (Top {a, b} \<circ> P)

goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i c. c <\<^bsub>(Top {a, b} \<circ> P) i\<^esub> f (Top {a, b} \<circ> P) \<longrightarrow> c <\<^bsub>(Top {a, b} \<circ> P') i\<^esub> f (Top {a, b} \<circ> P)
[PROOF STEP]
have "f (Top {a,b} \<circ> P) = f (Top {a,b} \<circ> P')"
[PROOF STATE]
proof (prove)
using this:
\<forall>i c. c <\<^bsub>(Top {a, b} \<circ> P) i\<^esub> f (Top {a, b} \<circ> P) \<longrightarrow> c <\<^bsub>(Top {a, b} \<circ> P') i\<^esub> f (Top {a, b} \<circ> P)

goal (1 subgoal):
 1. f (Top {a, b} \<circ> P) = f (Top {a, b} \<circ> P')
[PROOF STEP]
using Top_in_Prof[OF \<open>P:Prof\<close>] Top_in_Prof[OF \<open>P':Prof\<close>]
          mono[of "Top {a, b} \<circ> P"]
[PROOF STATE]
proof (prove)
using this:
\<forall>i c. c <\<^bsub>(Top {a, b} \<circ> P) i\<^esub> f (Top {a, b} \<circ> P) \<longrightarrow> c <\<^bsub>(Top {a, b} \<circ> P') i\<^esub> f (Top {a, b} \<circ> P)
Top ?S \<circ> P \<in> Prof
Top ?S \<circ> P' \<in> Prof
\<lbrakk>Top {a, b} \<circ> P \<in> Prof; ?P' \<in> Prof; \<forall>i aa. aa <\<^bsub>(Top {a, b} \<circ> P) i\<^esub> f (Top {a, b} \<circ> P) \<longrightarrow> aa <\<^bsub>?P' i\<^esub> f (Top {a, b} \<circ> P)\<rbrakk> \<Longrightarrow> f ?P' = f (Top {a, b} \<circ> P)

goal (1 subgoal):
 1. f (Top {a, b} \<circ> P) = f (Top {a, b} \<circ> P')
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
f (Top {a, b} \<circ> P) = f (Top {a, b} \<circ> P')

goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
thus "(a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)"
[PROOF STATE]
proof (prove)
using this:
f (Top {a, b} \<circ> P) = f (Top {a, b} \<circ> P')

goal (1 subgoal):
 1. (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
by(simp add: swf_def)
[PROOF STATE]
proof (state)
this:
(a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_dovetail_prim: "prim_recfn 2 r_dovetail"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prim_recfn 2 r_dovetail
[PROOF STEP]
by (simp add: r_dovetail_def)


[STATEMENT]
lemma abs_pred_stermI[intro]:
  assumes "\<And>cs. (\<And>pat t. (pat, t) \<in> set cs \<Longrightarrow> P t) \<Longrightarrow> P (Sabs cs)"
  shows "abs_pred P t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_pred P t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<And>pat t. (pat, t) \<in> set ?cs \<Longrightarrow> P t) \<Longrightarrow> P (Sabs ?cs)

goal (1 subgoal):
 1. abs_pred P t
[PROOF STEP]
unfolding abs_pred_sterm_def
[PROOF STATE]
proof (prove)
using this:
(\<And>pat t. (pat, t) \<in> set ?cs \<Longrightarrow> P t) \<Longrightarrow> P (Sabs ?cs)

goal (1 subgoal):
 1. \<forall>cs. t = Sabs cs \<longrightarrow> (\<forall>pat t. (pat, t) \<in> set cs \<longrightarrow> P t) \<longrightarrow> P t
[PROOF STEP]
by auto


[STATEMENT]
lemma is_binqueue_delete_min:
  assumes "is_binqueue 0 xs"
  shows "is_binqueue 0 (delete_min xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_binqueue 0 (delete_min xs)
[PROOF STEP]
proof (cases "find_min xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
 2. \<And>a. find_min xs = Some a \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
case (Some t)
[PROOF STATE]
proof (state)
this:
find_min xs = Some t

goal (2 subgoals):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
 2. \<And>a. find_min xs = Some a \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue 0 xs
[PROOF STEP]
have "is_binqueue 0 (map (match (priority t)) xs)"
[PROOF STATE]
proof (prove)
using this:
is_binqueue 0 xs

goal (1 subgoal):
 1. is_binqueue 0 (map (match (priority t)) xs)
[PROOF STEP]
by (induct xs) simp_all
[PROOF STATE]
proof (state)
this:
is_binqueue 0 (map (match (priority t)) xs)

goal (2 subgoals):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
 2. \<And>a. find_min xs = Some a \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_binqueue 0 (map (match (priority t)) xs)

goal (2 subgoals):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
 2. \<And>a. find_min xs = Some a \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
from Some
[PROOF STATE]
proof (chain)
picking this:
find_min xs = Some t
[PROOF STEP]
have "Some t \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
find_min xs = Some t

goal (1 subgoal):
 1. Some t \<in> set xs
[PROOF STEP]
by (rule find_min_exist)
[PROOF STATE]
proof (state)
this:
Some t \<in> set xs

goal (2 subgoals):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
 2. \<And>a. find_min xs = Some a \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue 0 xs
Some t \<in> set xs
[PROOF STEP]
have "\<exists>l. is_bintree l t" and "is_heap t"
[PROOF STATE]
proof (prove)
using this:
is_binqueue 0 xs
Some t \<in> set xs

goal (1 subgoal):
 1. \<exists>l. is_bintree_list l (children t) &&& is_heap_list (priority t) (children t)
[PROOF STEP]
using is_binqueue_select[of 0 xs t]
[PROOF STATE]
proof (prove)
using this:
is_binqueue 0 xs
Some t \<in> set xs
\<lbrakk>is_binqueue 0 xs; Some t \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>k. is_bintree_list k (children t) \<and> is_heap_list (priority t) (children t)

goal (1 subgoal):
 1. \<exists>l. is_bintree_list l (children t) &&& is_heap_list (priority t) (children t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l. is_bintree_list l (children t)
is_heap_list (priority t) (children t)

goal (2 subgoals):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
 2. \<And>a. find_min xs = Some a \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue 0 xs
\<exists>l. is_bintree_list l (children t)
is_heap_list (priority t) (children t)
[PROOF STEP]
have "is_binqueue 0 (map Some (rev (children t)))"
[PROOF STATE]
proof (prove)
using this:
is_binqueue 0 xs
\<exists>l. is_bintree_list l (children t)
is_heap_list (priority t) (children t)

goal (1 subgoal):
 1. is_binqueue 0 (map Some (rev (children t)))
[PROOF STEP]
by (auto simp add: is_binqueue_children)
[PROOF STATE]
proof (state)
this:
is_binqueue 0 (map Some (rev (children t)))

goal (2 subgoals):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
 2. \<And>a. find_min xs = Some a \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_binqueue 0 (map (match (priority t)) xs)
is_binqueue 0 (map Some (rev (children t)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_binqueue 0 (map (match (priority t)) xs)
is_binqueue 0 (map Some (rev (children t)))

goal (1 subgoal):
 1. is_binqueue 0 (delete_min xs)
[PROOF STEP]
using Some
[PROOF STATE]
proof (prove)
using this:
is_binqueue 0 (map (match (priority t)) xs)
is_binqueue 0 (map Some (rev (children t)))
find_min xs = Some t

goal (1 subgoal):
 1. is_binqueue 0 (delete_min xs)
[PROOF STEP]
by (auto simp add: is_binqueue_meld delete_min_def is_binqueue_normalize
      split: bintree.split)
[PROOF STATE]
proof (state)
this:
is_binqueue 0 (delete_min xs)

goal (1 subgoal):
 1. find_min xs = None \<Longrightarrow> is_binqueue 0 (delete_min xs)
[PROOF STEP]
qed (simp add: delete_min_def)


[STATEMENT]
lemma interleave_cont_rev_conc[simp]: "b@a \<in> a\<otimes>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b @ a \<in> a \<otimes> b
[PROOF STEP]
apply (subgoal_tac "b@a \<in> b\<otimes>a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b @ a \<in> b \<otimes> a \<Longrightarrow> b @ a \<in> a \<otimes> b
 2. b @ a \<in> b \<otimes> a
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b @ a \<in> b \<otimes> a
[PROOF STEP]
apply(simp only: interleave_cont_conc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ex_dist_less:
  assumes "c \<in> carrier Q\<^sub>p"
  shows "\<exists> a \<in> carrier Q\<^sub>p. val (a \<ominus> c) < \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a\<in>carrier Q\<^sub>p. val (a \<ominus> c) < \<beta>
[PROOF STEP]
using ex_val_less[of \<beta>] assms
[PROOF STATE]
proof (prove)
using this:
\<exists>\<alpha>. \<alpha> < \<beta>
c \<in> carrier Q\<^sub>p

goal (1 subgoal):
 1. \<exists>a\<in>carrier Q\<^sub>p. val (a \<ominus> c) < \<beta>
[PROOF STEP]
by (metis dist_nonempty' ex_val_less)


[STATEMENT]
lemma list_set_UNION_autoref[autoref_rules]:
      assumes "PRIO_TAG_OPTIMIZATION"
      assumes "SIDE_PRECOND_OPT (\<forall> x \<in> S. \<forall> y \<in> S. x \<noteq> y \<longrightarrow> g x \<inter> g y = {})"
      assumes "(xs, S) \<in> \<langle>A\<rangle> list_set_rel" "(f, g) \<in> A \<rightarrow> \<langle>B\<rangle> list_set_rel"
      shows "(xs \<bind> f,
        (OP (\<lambda>A f. \<Union> (f ` A)) ::: \<langle>A\<rangle> list_set_rel \<rightarrow> (A \<rightarrow> \<langle>B\<rangle> list_set_rel) \<rightarrow> \<langle>B\<rangle> list_set_rel) $ S $ g) \<in>
        \<langle>B\<rangle> list_set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<bind> f, (OP (\<lambda>A f. \<Union> (f ` A)) ::: \<langle>A\<rangle>list_set_rel \<rightarrow> (A \<rightarrow> \<langle>B\<rangle>list_set_rel) \<rightarrow> \<langle>B\<rangle>list_set_rel) $ S $ g) \<in> \<langle>B\<rangle>list_set_rel
[PROOF STEP]
using assms list_set_bind
[PROOF STATE]
proof (prove)
using this:
PRIO_TAG_OPTIMIZATION
SIDE_PRECOND_OPT (\<forall>x\<in>S. \<forall>y\<in>S. x \<noteq> y \<longrightarrow> g x \<inter> g y = {})
(xs, S) \<in> \<langle>A\<rangle>list_set_rel
(f, g) \<in> A \<rightarrow> \<langle>B\<rangle>list_set_rel
\<lbrakk>\<And>x y. \<lbrakk>x \<in> ?S; y \<in> ?S; x \<noteq> y\<rbrakk> \<Longrightarrow> ?g x \<inter> ?g y = {}; (?xs, ?S) \<in> \<langle>?A\<rangle>list_set_rel; (?f, ?g) \<in> ?A \<rightarrow> \<langle>?B\<rangle>list_set_rel\<rbrakk> \<Longrightarrow> (?xs \<bind> ?f, ?S \<bind> ?g) \<in> \<langle>?B\<rangle>list_set_rel

goal (1 subgoal):
 1. (xs \<bind> f, (OP (\<lambda>A f. \<Union> (f ` A)) ::: \<langle>A\<rangle>list_set_rel \<rightarrow> (A \<rightarrow> \<langle>B\<rangle>list_set_rel) \<rightarrow> \<langle>B\<rangle>list_set_rel) $ S $ g) \<in> \<langle>B\<rangle>list_set_rel
[PROOF STEP]
unfolding bind_UNION autoref_tag_defs
[PROOF STATE]
proof (prove)
using this:
PRIO_TAG_OPTIMIZATION
\<forall>x\<in>S. \<forall>y\<in>S. x \<noteq> y \<longrightarrow> g x \<inter> g y = {}
(xs, S) \<in> \<langle>A\<rangle>list_set_rel
(f, g) \<in> A \<rightarrow> \<langle>B\<rangle>list_set_rel
\<lbrakk>\<And>x y. \<lbrakk>x \<in> ?S; y \<in> ?S; x \<noteq> y\<rbrakk> \<Longrightarrow> ?g x \<inter> ?g y = {}; (?xs, ?S) \<in> \<langle>?A\<rangle>list_set_rel; (?f, ?g) \<in> ?A \<rightarrow> \<langle>?B\<rangle>list_set_rel\<rbrakk> \<Longrightarrow> (?xs \<bind> ?f, \<Union> (?g ` ?S)) \<in> \<langle>?B\<rangle>list_set_rel

goal (1 subgoal):
 1. (xs \<bind> f, \<Union> (g ` S)) \<in> \<langle>B\<rangle>list_set_rel
[PROOF STEP]
by metis


[STATEMENT]
theorem VSLuckyBlocks : "\<forall>xs. eval (VSLuckyBlocks \<phi>) xs = eval \<phi> xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs. eval (VSLuckyBlocks \<phi>) xs = eval \<phi> xs
[PROOF STEP]
unfolding VSLuckyBlocks_def Unpower_def opt_group_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs. eval ((push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers \<circ> QE_dnf' (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers) (the_real_step_augment luckyFind') \<circ> VSLuckiestBlocks \<circ> (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers)) \<phi>) xs = eval \<phi> xs
[PROOF STEP]
using QE_dnf'_eval[OF the_real_step_augment[OF luckyFind'_eval, of "\<lambda>x _ _. x"] opt]
[PROOF STATE]
proof (prove)
using this:
(\<And>amount F \<Gamma> xs var L Fa \<Gamma>'. length xs = var \<Longrightarrow> length xs = var) \<Longrightarrow> eval (QE_dnf' (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers) (the_real_step_augment luckyFind') ?\<phi>) ?xs = eval ?\<phi> ?xs

goal (1 subgoal):
 1. \<forall>xs. eval ((push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers \<circ> QE_dnf' (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers) (the_real_step_augment luckyFind') \<circ> VSLuckiestBlocks \<circ> (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers)) \<phi>) xs = eval \<phi> xs
[PROOF STEP]
using opt VSLuckiestBlocks
[PROOF STATE]
proof (prove)
using this:
(\<And>amount F \<Gamma> xs var L Fa \<Gamma>'. length xs = var \<Longrightarrow> length xs = var) \<Longrightarrow> eval (QE_dnf' (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers) (the_real_step_augment luckyFind') ?\<phi>) ?xs = eval ?\<phi> ?xs
eval ((push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers) ?F) ?L = eval ?F ?L
\<forall>xs. eval (VSLuckiestBlocks ?\<phi>) xs = eval ?\<phi> xs

goal (1 subgoal):
 1. \<forall>xs. eval ((push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers \<circ> QE_dnf' (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers) (the_real_step_augment luckyFind') \<circ> VSLuckiestBlocks \<circ> (push_forall \<circ> nnf \<circ> unpower 0 \<circ> groupQuantifiers \<circ> clearQuantifiers)) \<phi>) xs = eval \<phi> xs
[PROOF STEP]
by fastforce