[STATEMENT]
lemma dbl_neg: "- (-x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
have "\<bottom>\<bottom> = -(-x \<squnion> -(-x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom>\<bottom> = - (- x \<squnion> - (- x))
[PROOF STEP]
by (metis robbins sup_comm sup_ident)
[PROOF STATE]
proof (state)
this:
\<bottom>\<bottom> = - (- x \<squnion> - (- x))

goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<bottom>\<bottom> = - (- ?xa2 \<squnion> - (- ?xa2))

goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
note I = this
[PROOF STATE]
proof (state)
this:
\<bottom>\<bottom> = - (- ?xa2 \<squnion> - (- ?xa2))

goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<bottom>\<bottom> = - (- ?xa2 \<squnion> - (- ?xa2))

goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
have "-x = -(-(-x \<squnion> -(-(-x))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - x = - (- (- x \<squnion> - (- (- x))))
[PROOF STEP]
by (metis I robbins sup_comm sup_ident)
[PROOF STATE]
proof (state)
this:
- x = - (- (- x \<squnion> - (- (- x))))

goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
- ?xa2 = - (- (- ?xa2 \<squnion> - (- (- ?xa2))))

goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
note II = this
[PROOF STATE]
proof (state)
this:
- ?xa2 = - (- (- ?xa2 \<squnion> - (- (- ?xa2))))

goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
- ?xa2 = - (- (- ?xa2 \<squnion> - (- (- ?xa2))))

goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
have "-(-(-x)) = -(-(-x \<squnion> -(-(-x))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (- (- x)) = - (- (- x \<squnion> - (- (- x))))
[PROOF STEP]
by (metis I II robbins sup_assoc sup_comm sup_ident)
[PROOF STATE]
proof (state)
this:
- (- (- x)) = - (- (- x \<squnion> - (- (- x))))

goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
- (- (- ?xa2)) = - (- (- ?xa2 \<squnion> - (- (- ?xa2))))

goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
note III = this
[PROOF STATE]
proof (state)
this:
- (- (- ?xa2)) = - (- (- ?xa2 \<squnion> - (- (- ?xa2))))

goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (- x) = x
[PROOF STEP]
by (metis II III robbins)
[PROOF STATE]
proof (state)
this:
- (- x) = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rows_to_keep_lem:
  fixes A:: "('a::field) mat"
  shows "\<And>ell. ell \<in> set (rows_to_keep A) \<Longrightarrow> ell < dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ell. ell \<in> set (rows_to_keep A) \<Longrightarrow> ell < dim_row A
[PROOF STEP]
unfolding rows_to_keep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ell. ell \<in> set (map snd (pivot_positions (gauss_jordan_single A\<^sup>T))) \<Longrightarrow> ell < dim_row A
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set (pivot_positions (gauss_jordan_single A\<^sup>T)) \<Longrightarrow> b < dim_row A
[PROOF STEP]
using rref_pivot_positions
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>row_echelon_form ?R; ?R \<in> carrier_mat ?nr ?nc; (?i, ?j) \<in> set (pivot_positions ?R)\<rbrakk> \<Longrightarrow> ?i < ?nr \<and> ?j < ?nc

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set (pivot_positions (gauss_jordan_single A\<^sup>T)) \<Longrightarrow> b < dim_row A
[PROOF STEP]
by (metis carrier_mat_triv gauss_jordan_single(2) gauss_jordan_single(3) index_transpose_mat(3))


[STATEMENT]
lemma inext_singleton_cut_greater_empty_iff: "
  ({inext t0 I} \<down>> t0 = {}) = (I \<down>> t0 = {} \<or> t0 \<notin> I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({inext t0 I} \<down>> t0 = {}) = (I \<down>> t0 = {} \<or> t0 \<notin> I)
[PROOF STEP]
apply (subst Not_eq_iff[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({inext t0 I} \<down>> t0 \<noteq> {}) = (\<not> (I \<down>> t0 = {} \<or> t0 \<notin> I))
[PROOF STEP]
apply (simp add: inext_singleton_cut_greater_not_empty_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iLastWeak_iff : "(\<ominus>\<^sub>W t t0 I. P t) = ((\<ominus> t t0 I. P t) \<or> (I \<down>< t0 = {}) \<or> t0 \<notin> I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iLastWeak t0 I P = (iLast t0 I P \<or> I \<down>< t0 = {} \<or> t0 \<notin> I)
[PROOF STEP]
apply (unfold iTL_defs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>t\<in>{iprev t0 I} \<down>< t0. P t) = (P (iprev t0 I) \<or> I \<down>< t0 = {} \<or> t0 \<notin> I)
[PROOF STEP]
apply (simp add: iprev_singleton_cut_less_empty_iff[symmetric] cut_less_singleton)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iWeakUntil_True[simp]: "P t'. t' \<W> t I. True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P t'. t' \<W> t I. True
[PROOF STEP]
apply (simp add: iTL_defs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>t\<in>I. P t) \<or> (\<exists>t\<in>I. \<forall>x\<in>I \<down>< t. P x)
[PROOF STEP]
apply (case_tac "I = {}", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> (\<forall>t\<in>I. P t) \<or> (\<exists>t\<in>I. \<forall>x\<in>I \<down>< t. P x)
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> \<exists>t\<in>I. \<forall>x\<in>I \<down>< t. P x
[PROOF STEP]
apply (rule_tac x="iMin I" in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. I \<noteq> {} \<Longrightarrow> \<forall>x\<in>I \<down>< iMin I. P x
 2. I \<noteq> {} \<Longrightarrow> iMin I \<in> I
[PROOF STEP]
apply (simp add: cut_less_Min_empty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> iMin I \<in> I
[PROOF STEP]
apply (simp add: iMinI_ex2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prefixes_nontotal_hyp:
  assumes "prefixes t j \<down>= b"
    and "prefixes (Suc t) j \<up>"
    and "s b \<down>= i"
  shows "\<exists>x. \<phi> i x \<up>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. \<phi> i x \<up>
[PROOF STEP]
using nxt_nontotal_hyp[OF _ assms(3)] assms(2) prefixes_at_Suc'[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
nxt b \<up> \<Longrightarrow> \<exists>x. \<phi> i x \<up>
local.prefixes (Suc t) j \<up>
local.prefixes (Suc t) j = nxt b

goal (1 subgoal):
 1. \<exists>x. \<phi> i x \<up>
[PROOF STEP]
by simp


[STATEMENT]
lemma inv_loop5_Oc_via_4_Bk[elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)
[PROOF STEP]
by (auto simp: inv_loop4.simps inv_loop5.simps)


[STATEMENT]
lemma labeled_saturation_lifting: "saturated NL \<Longrightarrow> no_labels.saturated (fst ` NL)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. saturated NL \<Longrightarrow> local.no_labels.saturated (fst ` NL)
[PROOF STEP]
unfolding saturated_def no_labels.saturated_def Inf_from_def no_labels.Inf_from_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL \<Longrightarrow> {\<iota> \<in> Inf_F. set (prems_of \<iota>) \<subseteq> fst ` NL} \<subseteq> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
fix \<iota>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
assume
    subs_Red_I: "{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL" and
    i_in: "\<iota> \<in> Inf_F" and
    i_prems: "set (prems_of \<iota>) \<subseteq> fst ` NL"
[PROOF STATE]
proof (state)
this:
{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL
\<iota> \<in> Inf_F
set (prems_of \<iota>) \<subseteq> fst ` NL

goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
define Lli where "Lli i = (SOME x. ((prems_of \<iota>)!i,x) \<in> NL)" for i
[PROOF STATE]
proof (state)
this:
Lli ?i = (SOME x. (prems_of \<iota> ! ?i, x) \<in> NL)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
have [simp]:"((prems_of \<iota>)!i,Lli i) \<in> NL" if "i < length (prems_of \<iota>)" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (prems_of \<iota> ! i, Lli i) \<in> NL
[PROOF STEP]
using that i_prems
[PROOF STATE]
proof (prove)
using this:
i < length (prems_of \<iota>)
set (prems_of \<iota>) \<subseteq> fst ` NL

goal (1 subgoal):
 1. (prems_of \<iota> ! i, Lli i) \<in> NL
[PROOF STEP]
unfolding Lli_def
[PROOF STATE]
proof (prove)
using this:
i < length (prems_of \<iota>)
set (prems_of \<iota>) \<subseteq> fst ` NL

goal (1 subgoal):
 1. (prems_of \<iota> ! i, SOME x. (prems_of \<iota> ! i, x) \<in> NL) \<in> NL
[PROOF STEP]
by (metis nth_mem someI_ex DomainE Domain_fst subset_eq)
[PROOF STATE]
proof (state)
this:
?i < length (prems_of \<iota>) \<Longrightarrow> (prems_of \<iota> ! ?i, Lli ?i) \<in> NL

goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
define Ll where "Ll = map Lli [0..<length (prems_of \<iota>)]"
[PROOF STATE]
proof (state)
this:
Ll = map Lli [0..<length (prems_of \<iota>)]

goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
have Ll_length: "length Ll = length (prems_of \<iota>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length Ll = length (prems_of \<iota>)
[PROOF STEP]
unfolding Ll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map Lli [0..<length (prems_of \<iota>)]) = length (prems_of \<iota>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length Ll = length (prems_of \<iota>)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
have subs_NL: "set (zip (prems_of \<iota>) Ll) \<subseteq> NL"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (zip (prems_of \<iota>) Ll) \<subseteq> NL
[PROOF STEP]
unfolding Ll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (zip (prems_of \<iota>) (map Lli [0..<length (prems_of \<iota>)])) \<subseteq> NL
[PROOF STEP]
by (auto simp:in_set_zip)
[PROOF STATE]
proof (state)
this:
set (zip (prems_of \<iota>) Ll) \<subseteq> NL

goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
obtain L0 where L0: "Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0) \<in> Inf_FL"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>L0. Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0) \<in> Inf_FL \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Inf_F_to_Inf_FL[OF i_in Ll_length]
[PROOF STATE]
proof (prove)
using this:
\<exists>L0. Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0) \<in> Inf_FL

goal (1 subgoal):
 1. (\<And>L0. Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0) \<in> Inf_FL \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0) \<in> Inf_FL

goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
define \<iota>_FL where "\<iota>_FL = Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0)"
[PROOF STATE]
proof (state)
this:
\<iota>_FL = Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<iota>_FL = Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0)
[PROOF STEP]
have "set (prems_of \<iota>_FL) \<subseteq> NL"
[PROOF STATE]
proof (prove)
using this:
\<iota>_FL = Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0)

goal (1 subgoal):
 1. set (prems_of \<iota>_FL) \<subseteq> NL
[PROOF STEP]
using subs_NL
[PROOF STATE]
proof (prove)
using this:
\<iota>_FL = Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0)
set (zip (prems_of \<iota>) Ll) \<subseteq> NL

goal (1 subgoal):
 1. set (prems_of \<iota>_FL) \<subseteq> NL
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (prems_of \<iota>_FL) \<subseteq> NL

goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (prems_of \<iota>_FL) \<subseteq> NL
[PROOF STEP]
have "\<iota>_FL \<in> {\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL}"
[PROOF STATE]
proof (prove)
using this:
set (prems_of \<iota>_FL) \<subseteq> NL

goal (1 subgoal):
 1. \<iota>_FL \<in> {\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL}
[PROOF STEP]
unfolding \<iota>_FL_def
[PROOF STATE]
proof (prove)
using this:
set (prems_of (Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0))) \<subseteq> NL

goal (1 subgoal):
 1. Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0) \<in> {\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL}
[PROOF STEP]
using L0
[PROOF STATE]
proof (prove)
using this:
set (prems_of (Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0))) \<subseteq> NL
Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0) \<in> Inf_FL

goal (1 subgoal):
 1. Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0) \<in> {\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<iota>_FL \<in> {\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<iota>_FL \<in> {\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL}
[PROOF STEP]
have "\<iota>_FL \<in> Red_I_\<G> NL"
[PROOF STATE]
proof (prove)
using this:
\<iota>_FL \<in> {\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL}

goal (1 subgoal):
 1. \<iota>_FL \<in> Red_I_\<G> NL
[PROOF STEP]
using subs_Red_I
[PROOF STATE]
proof (prove)
using this:
\<iota>_FL \<in> {\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL}
{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL

goal (1 subgoal):
 1. \<iota>_FL \<in> Red_I_\<G> NL
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<iota>_FL \<in> Red_I_\<G> NL

goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<iota>_FL \<in> Red_I_\<G> NL

goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
have "\<iota> = to_F \<iota>_FL"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota> = to_F \<iota>_FL
[PROOF STEP]
unfolding to_F_def \<iota>_FL_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota> = Infer (map fst (prems_of (Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0)))) (fst (concl_of (Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0))))
[PROOF STEP]
using Ll_length
[PROOF STATE]
proof (prove)
using this:
length Ll = length (prems_of \<iota>)

goal (1 subgoal):
 1. \<iota> = Infer (map fst (prems_of (Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0)))) (fst (concl_of (Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0))))
[PROOF STEP]
by (cases \<iota>) auto
[PROOF STATE]
proof (state)
this:
\<iota> = to_F \<iota>_FL

goal (1 subgoal):
 1. \<And>x. \<lbrakk>{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> Red_I_\<G> NL; x \<in> Inf_F; set (prems_of x) \<subseteq> fst ` NL\<rbrakk> \<Longrightarrow> x \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<iota>_FL \<in> Red_I_\<G> NL
\<iota> = to_F \<iota>_FL
[PROOF STEP]
show "\<iota> \<in> no_labels.Red_I_\<G> (fst ` NL)"
[PROOF STATE]
proof (prove)
using this:
\<iota>_FL \<in> Red_I_\<G> NL
\<iota> = to_F \<iota>_FL

goal (1 subgoal):
 1. \<iota> \<in> no_labels.Red_I_\<G> (fst ` NL)
[PROOF STEP]
by (auto intro: red_inf_impl)
[PROOF STATE]
proof (state)
this:
\<iota> \<in> no_labels.Red_I_\<G> (fst ` NL)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chain_construct_2:
    assumes "P 0 x\<^sub>0" "\<And> k x. P k x \<Longrightarrow> \<exists> x'. P (Suc k) x' \<and> f x \<le> f x' \<and> g x \<le> g x'"
    assumes "\<And> k x. P k x \<Longrightarrow> k \<le> length (f x)" "\<And> k x. P k x \<Longrightarrow> k \<le> length (g x)"
    obtains Q
    where "\<And> k. P k (Q k)" "chain (f \<circ> Q)" "chain (g \<circ> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>\<And>k. P k (Q k); chain (f \<circ> Q); chain (g \<circ> Q)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>\<And>k. P k (Q k); chain (f \<circ> Q); chain (g \<circ> Q)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain x' where 1:
      "P 0 x\<^sub>0" "\<And> k x. P k x \<Longrightarrow> P (Suc k) (x' k x) \<and> f x \<le> f (x' k x) \<and> g x \<le> g (x' k x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>P 0 x\<^sub>0; \<And>k x. P k x \<Longrightarrow> P (Suc k) (x' k x) \<and> f x \<le> f (x' k x) \<and> g x \<le> g (x' k x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1, 2)
[PROOF STATE]
proof (prove)
using this:
P 0 x\<^sub>0
P ?k ?x \<Longrightarrow> \<exists>x'. P (Suc ?k) x' \<and> f ?x \<le> f x' \<and> g ?x \<le> g x'

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>P 0 x\<^sub>0; \<And>k x. P k x \<Longrightarrow> P (Suc k) (x' k x) \<and> f x \<le> f (x' k x) \<and> g x \<le> g (x' k x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
P 0 x\<^sub>0
P ?k ?x \<Longrightarrow> P (Suc ?k) (x' ?k ?x) \<and> f ?x \<le> f (x' ?k ?x) \<and> g ?x \<le> g (x' ?k ?x)

goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>\<And>k. P k (Q k); chain (f \<circ> Q); chain (g \<circ> Q)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define Q where "Q \<equiv> rec_nat x\<^sub>0 x'"
[PROOF STATE]
proof (state)
this:
Q \<equiv> rec_nat x\<^sub>0 x'

goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>\<And>k. P k (Q k); chain (f \<circ> Q); chain (g \<circ> Q)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have [simp]: "Q 0 = x\<^sub>0" "\<And> k. Q (Suc k) = x' k (Q k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q 0 = x\<^sub>0 &&& (\<And>k. Q (Suc k) = x' k (Q k))
[PROOF STEP]
unfolding Q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_nat x\<^sub>0 x' 0 = x\<^sub>0 &&& (\<And>k. rec_nat x\<^sub>0 x' (Suc k) = x' k (rec_nat x\<^sub>0 x' k))
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
Q 0 = x\<^sub>0
Q (Suc ?k) = x' ?k (Q ?k)

goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>\<And>k. P k (Q k); chain (f \<circ> Q); chain (g \<circ> Q)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have 2: "\<And> k. P k (Q k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. P k (Q k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. P k (Q k)
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. P k (Q k)
[PROOF STEP]
show "P k (Q k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P k (Q k)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
P 0 x\<^sub>0
P ?k ?x \<Longrightarrow> P (Suc ?k) (x' ?k ?x) \<and> f ?x \<le> f (x' ?k ?x) \<and> g ?x \<le> g (x' ?k ?x)

goal (1 subgoal):
 1. P k (Q k)
[PROOF STEP]
by (induct k, auto)
[PROOF STATE]
proof (state)
this:
P k (Q k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P ?k (Q ?k)

goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>\<And>k. P k (Q k); chain (f \<circ> Q); chain (g \<circ> Q)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (intro that chainI monoI, unfold comp_apply)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>k. P k (?Q k)
 2. \<And>x y. x \<le> y \<Longrightarrow> f (?Q x) \<le> f (?Q y)
 3. \<And>k. \<exists>l. k < length (f (?Q l))
 4. \<And>x y. x \<le> y \<Longrightarrow> g (?Q x) \<le> g (?Q y)
 5. \<And>k. \<exists>l. k < length (g (?Q l))
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>k. P k (?Q k)
 2. \<And>x y. x \<le> y \<Longrightarrow> f (?Q x) \<le> f (?Q y)
 3. \<And>k. \<exists>l. k < length (f (?Q l))
 4. \<And>x y. x \<le> y \<Longrightarrow> g (?Q x) \<le> g (?Q y)
 5. \<And>k. \<exists>l. k < length (g (?Q l))
[PROOF STEP]
show "P k (Q k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P k (Q k)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
P ?k (Q ?k)

goal (1 subgoal):
 1. P k (Q k)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
P k (Q k)

goal (4 subgoals):
 1. \<And>x y. x \<le> y \<Longrightarrow> f (Q x) \<le> f (Q y)
 2. \<And>k. \<exists>l. k < length (f (Q l))
 3. \<And>x y. x \<le> y \<Longrightarrow> g (Q x) \<le> g (Q y)
 4. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x y. x \<le> y \<Longrightarrow> f (Q x) \<le> f (Q y)
 2. \<And>k. \<exists>l. k < length (f (Q l))
 3. \<And>x y. x \<le> y \<Longrightarrow> g (Q x) \<le> g (Q y)
 4. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
fix x y :: nat
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x y. x \<le> y \<Longrightarrow> f (Q x) \<le> f (Q y)
 2. \<And>k. \<exists>l. k < length (f (Q l))
 3. \<And>x y. x \<le> y \<Longrightarrow> g (Q x) \<le> g (Q y)
 4. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
assume "x \<le> y"
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (4 subgoals):
 1. \<And>x y. x \<le> y \<Longrightarrow> f (Q x) \<le> f (Q y)
 2. \<And>k. \<exists>l. k < length (f (Q l))
 3. \<And>x y. x \<le> y \<Longrightarrow> g (Q x) \<le> g (Q y)
 4. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
thus "f (Q x) \<le> f (Q y)"
[PROOF STATE]
proof (prove)
using this:
x \<le> y

goal (1 subgoal):
 1. f (Q x) \<le> f (Q y)
[PROOF STEP]
proof (induct "y - x" arbitrary: x y)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>0 = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y)
 2. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = y - x
x \<le> y

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>0 = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y)
 2. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Q x) \<le> f (Q y)
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
0 = y - x
x \<le> y

goal (1 subgoal):
 1. f (Q x) \<le> f (Q y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (Q x) \<le> f (Q y)

goal (1 subgoal):
 1. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k = ?y - ?x; ?x \<le> ?y\<rbrakk> \<Longrightarrow> f (Q ?x) \<le> f (Q ?y)
Suc k = y - x
x \<le> y

goal (1 subgoal):
 1. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y)
[PROOF STEP]
have "f (Q x) \<le> f (Q (Suc x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Q x) \<le> f (Q (Suc x))
[PROOF STEP]
using 1(2) 2
[PROOF STATE]
proof (prove)
using this:
P ?k ?x \<Longrightarrow> P (Suc ?k) (x' ?k ?x) \<and> f ?x \<le> f (x' ?k ?x) \<and> g ?x \<le> g (x' ?k ?x)
P ?k (Q ?k)

goal (1 subgoal):
 1. f (Q x) \<le> f (Q (Suc x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (Q x) \<le> f (Q (Suc x))

goal (1 subgoal):
 1. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (Q x) \<le> f (Q (Suc x))

goal (1 subgoal):
 1. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y)
[PROOF STEP]
have "\<dots> \<le> f (Q y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Q (Suc x)) \<le> f (Q y)
[PROOF STEP]
using Suc(2)
[PROOF STATE]
proof (prove)
using this:
Suc k = y - x

goal (1 subgoal):
 1. f (Q (Suc x)) \<le> f (Q y)
[PROOF STEP]
by (intro Suc(1), auto)
[PROOF STATE]
proof (state)
this:
f (Q (Suc x)) \<le> f (Q y)

goal (1 subgoal):
 1. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> f (Q x) \<le> f (Q y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f (Q x) \<le> f (Q y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
f (Q x) \<le> f (Q y)

goal (1 subgoal):
 1. f (Q x) \<le> f (Q y)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
f (Q x) \<le> f (Q y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (Q x) \<le> f (Q y)

goal (3 subgoals):
 1. \<And>k. \<exists>l. k < length (f (Q l))
 2. \<And>x y. x \<le> y \<Longrightarrow> g (Q x) \<le> g (Q y)
 3. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k. \<exists>l. k < length (f (Q l))
 2. \<And>x y. x \<le> y \<Longrightarrow> g (Q x) \<le> g (Q y)
 3. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k. \<exists>l. k < length (f (Q l))
 2. \<And>x y. x \<le> y \<Longrightarrow> g (Q x) \<le> g (Q y)
 3. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
have 3: "P (Suc k) (Q (Suc k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (Suc k) (Q (Suc k))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
P ?k (Q ?k)

goal (1 subgoal):
 1. P (Suc k) (Q (Suc k))
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
P (Suc k) (Q (Suc k))

goal (3 subgoals):
 1. \<And>k. \<exists>l. k < length (f (Q l))
 2. \<And>x y. x \<le> y \<Longrightarrow> g (Q x) \<le> g (Q y)
 3. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
have 4: "Suc k \<le> length (f (Q (Suc k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc k \<le> length (f (Q (Suc k)))
[PROOF STEP]
using assms(3) 3
[PROOF STATE]
proof (prove)
using this:
P ?k ?x \<Longrightarrow> ?k \<le> length (f ?x)
P (Suc k) (Q (Suc k))

goal (1 subgoal):
 1. Suc k \<le> length (f (Q (Suc k)))
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
Suc k \<le> length (f (Q (Suc k)))

goal (3 subgoals):
 1. \<And>k. \<exists>l. k < length (f (Q l))
 2. \<And>x y. x \<le> y \<Longrightarrow> g (Q x) \<le> g (Q y)
 3. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
have 5: "k < length (f (Q (Suc k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < length (f (Q (Suc k)))
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
Suc k \<le> length (f (Q (Suc k)))

goal (1 subgoal):
 1. k < length (f (Q (Suc k)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k < length (f (Q (Suc k)))

goal (3 subgoals):
 1. \<And>k. \<exists>l. k < length (f (Q l))
 2. \<And>x y. x \<le> y \<Longrightarrow> g (Q x) \<le> g (Q y)
 3. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
show "\<exists> l. k < length (f (Q l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. k < length (f (Q l))
[PROOF STEP]
using 5
[PROOF STATE]
proof (prove)
using this:
k < length (f (Q (Suc k)))

goal (1 subgoal):
 1. \<exists>l. k < length (f (Q l))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>l. k < length (f (Q l))

goal (2 subgoals):
 1. \<And>x y. x \<le> y \<Longrightarrow> g (Q x) \<le> g (Q y)
 2. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. x \<le> y \<Longrightarrow> g (Q x) \<le> g (Q y)
 2. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
fix x y :: nat
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. x \<le> y \<Longrightarrow> g (Q x) \<le> g (Q y)
 2. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
assume "x \<le> y"
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (2 subgoals):
 1. \<And>x y. x \<le> y \<Longrightarrow> g (Q x) \<le> g (Q y)
 2. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
thus "g (Q x) \<le> g (Q y)"
[PROOF STATE]
proof (prove)
using this:
x \<le> y

goal (1 subgoal):
 1. g (Q x) \<le> g (Q y)
[PROOF STEP]
proof (induct "y - x" arbitrary: x y)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>0 = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y)
 2. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = y - x
x \<le> y

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>0 = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y)
 2. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (Q x) \<le> g (Q y)
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
0 = y - x
x \<le> y

goal (1 subgoal):
 1. g (Q x) \<le> g (Q y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g (Q x) \<le> g (Q y)

goal (1 subgoal):
 1. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k = ?y - ?x; ?x \<le> ?y\<rbrakk> \<Longrightarrow> g (Q ?x) \<le> g (Q ?y)
Suc k = y - x
x \<le> y

goal (1 subgoal):
 1. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y)
[PROOF STEP]
have "g (Q x) \<le> g (Q (Suc x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (Q x) \<le> g (Q (Suc x))
[PROOF STEP]
using 1(2) 2
[PROOF STATE]
proof (prove)
using this:
P ?k ?x \<Longrightarrow> P (Suc ?k) (x' ?k ?x) \<and> f ?x \<le> f (x' ?k ?x) \<and> g ?x \<le> g (x' ?k ?x)
P ?k (Q ?k)

goal (1 subgoal):
 1. g (Q x) \<le> g (Q (Suc x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g (Q x) \<le> g (Q (Suc x))

goal (1 subgoal):
 1. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
g (Q x) \<le> g (Q (Suc x))

goal (1 subgoal):
 1. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y)
[PROOF STEP]
have "\<dots> \<le> g (Q y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (Q (Suc x)) \<le> g (Q y)
[PROOF STEP]
using Suc(2)
[PROOF STATE]
proof (prove)
using this:
Suc k = y - x

goal (1 subgoal):
 1. g (Q (Suc x)) \<le> g (Q y)
[PROOF STEP]
by (intro Suc(1), auto)
[PROOF STATE]
proof (state)
this:
g (Q (Suc x)) \<le> g (Q y)

goal (1 subgoal):
 1. \<And>xa x y. \<lbrakk>\<And>x y. \<lbrakk>xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y); Suc xa = y - x; x \<le> y\<rbrakk> \<Longrightarrow> g (Q x) \<le> g (Q y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
g (Q x) \<le> g (Q y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
g (Q x) \<le> g (Q y)

goal (1 subgoal):
 1. g (Q x) \<le> g (Q y)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
g (Q x) \<le> g (Q y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g (Q x) \<le> g (Q y)

goal (1 subgoal):
 1. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
have 3: "P (Suc k) (Q (Suc k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (Suc k) (Q (Suc k))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
P ?k (Q ?k)

goal (1 subgoal):
 1. P (Suc k) (Q (Suc k))
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
P (Suc k) (Q (Suc k))

goal (1 subgoal):
 1. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
have 4: "Suc k \<le> length (g (Q (Suc k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc k \<le> length (g (Q (Suc k)))
[PROOF STEP]
using assms(4) 3
[PROOF STATE]
proof (prove)
using this:
P ?k ?x \<Longrightarrow> ?k \<le> length (g ?x)
P (Suc k) (Q (Suc k))

goal (1 subgoal):
 1. Suc k \<le> length (g (Q (Suc k)))
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
Suc k \<le> length (g (Q (Suc k)))

goal (1 subgoal):
 1. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
have 5: "k < length (g (Q (Suc k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < length (g (Q (Suc k)))
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
Suc k \<le> length (g (Q (Suc k)))

goal (1 subgoal):
 1. k < length (g (Q (Suc k)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k < length (g (Q (Suc k)))

goal (1 subgoal):
 1. \<And>k. \<exists>l. k < length (g (Q l))
[PROOF STEP]
show "\<exists> l. k < length (g (Q l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. k < length (g (Q l))
[PROOF STEP]
using 5
[PROOF STATE]
proof (prove)
using this:
k < length (g (Q (Suc k)))

goal (1 subgoal):
 1. \<exists>l. k < length (g (Q l))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>l. k < length (g (Q l))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nth'_0 [simp]: "nth' (x # xs) 0 = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth' (x # xs) 0 = x
[PROOF STEP]
by (simp add: nth'_def)


[STATEMENT]
lemma ts_okD:
  "\<And>ln. \<lbrakk> ts_ok P ts m; ts t = \<lfloor>(x, ln)\<rfloor> \<rbrakk> \<Longrightarrow> P t x m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ln. \<lbrakk>ts_ok P ts m; ts t = \<lfloor>(x, ln)\<rfloor>\<rbrakk> \<Longrightarrow> P t x m
[PROOF STEP]
by(auto simp add: ts_ok_def)


[STATEMENT]
lemma lfilled_deterministic:
  assumes "Lfilled k lfilled es les"
          "Lfilled k lfilled es les'"
  shows "les = les'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. les = les'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Lfilled k lfilled es les
Lfilled k lfilled es les'

goal (1 subgoal):
 1. les = les'
[PROOF STEP]
proof (induction arbitrary: les' rule: Lfilled.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>vs lholed es' es les'. \<lbrakk>const_list vs; lholed = LBase vs es'; Lfilled 0 lholed es les'\<rbrakk> \<Longrightarrow> vs @ es @ es' = les'
 2. \<And>vs lholed n es' l es'' k es lfilledk les'. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled k l es lfilledk; \<And>les'. Lfilled k l es les' \<Longrightarrow> lfilledk = les'; Lfilled (k + 1) lholed es les'\<rbrakk> \<Longrightarrow> vs @ [Label n es' lfilledk] @ es'' = les'
[PROOF STEP]
case (L0 vs lholed es' es)
[PROOF STATE]
proof (state)
this:
const_list vs
lholed = LBase vs es'
Lfilled 0 lholed es les'

goal (2 subgoals):
 1. \<And>vs lholed es' es les'. \<lbrakk>const_list vs; lholed = LBase vs es'; Lfilled 0 lholed es les'\<rbrakk> \<Longrightarrow> vs @ es @ es' = les'
 2. \<And>vs lholed n es' l es'' k es lfilledk les'. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled k l es lfilledk; \<And>les'. Lfilled k l es les' \<Longrightarrow> lfilledk = les'; Lfilled (k + 1) lholed es les'\<rbrakk> \<Longrightarrow> vs @ [Label n es' lfilledk] @ es'' = les'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
const_list vs
lholed = LBase vs es'
Lfilled 0 lholed es les'

goal (1 subgoal):
 1. vs @ es @ es' = les'
[PROOF STEP]
by (fastforce simp add: Lfilled.simps[of 0])
[PROOF STATE]
proof (state)
this:
vs @ es @ es' = les'

goal (1 subgoal):
 1. \<And>vs lholed n es' l es'' k es lfilledk les'. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled k l es lfilledk; \<And>les'. Lfilled k l es les' \<Longrightarrow> lfilledk = les'; Lfilled (k + 1) lholed es les'\<rbrakk> \<Longrightarrow> vs @ [Label n es' lfilledk] @ es'' = les'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>vs lholed n es' l es'' k es lfilledk les'. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled k l es lfilledk; \<And>les'. Lfilled k l es les' \<Longrightarrow> lfilledk = les'; Lfilled (k + 1) lholed es les'\<rbrakk> \<Longrightarrow> vs @ [Label n es' lfilledk] @ es'' = les'
[PROOF STEP]
case (LN vs lholed n es' l es'' k es lfilledk)
[PROOF STATE]
proof (state)
this:
const_list vs
lholed = LRec vs n es' l es''
Lfilled k l es lfilledk
Lfilled k l es ?les' \<Longrightarrow> lfilledk = ?les'
Lfilled (k + 1) lholed es les'

goal (1 subgoal):
 1. \<And>vs lholed n es' l es'' k es lfilledk les'. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled k l es lfilledk; \<And>les'. Lfilled k l es les' \<Longrightarrow> lfilledk = les'; Lfilled (k + 1) lholed es les'\<rbrakk> \<Longrightarrow> vs @ [Label n es' lfilledk] @ es'' = les'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
const_list vs
lholed = LRec vs n es' l es''
Lfilled k l es lfilledk
Lfilled k l es ?les' \<Longrightarrow> lfilledk = ?les'
Lfilled (k + 1) lholed es les'

goal (1 subgoal):
 1. vs @ [Label n es' lfilledk] @ es'' = les'
[PROOF STEP]
unfolding Lfilled.simps[of "(k + 1)"]
[PROOF STATE]
proof (prove)
using this:
const_list vs
lholed = LRec vs n es' l es''
Lfilled k l es lfilledk
Lfilled k l es ?les' \<Longrightarrow> lfilledk = ?les'
(\<exists>vs lholeda es' es. k + 1 = 0 \<and> lholed = lholeda \<and> es = es \<and> les' = vs @ es @ es' \<and> const_list vs \<and> lholeda = LBase vs es') \<or> (\<exists>vs lholeda n es' l es'' k es lfilledk. k + 1 = k + 1 \<and> lholed = lholeda \<and> es = es \<and> les' = vs @ [Label n es' lfilledk] @ es'' \<and> const_list vs \<and> lholeda = LRec vs n es' l es'' \<and> Lfilled k l es lfilledk)

goal (1 subgoal):
 1. vs @ [Label n es' lfilledk] @ es'' = les'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
vs @ [Label n es' lfilledk] @ es'' = les'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chop_subst_emb:
  assumes "is_App s"
  shows "chop (subst \<rho> s) \<unrhd>\<^sub>e\<^sub>m\<^sub>b subst \<rho> (chop s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chop (subst \<rho> s) \<unrhd>\<^sub>e\<^sub>m\<^sub>b subst \<rho> (chop s)
[PROOF STEP]
using chop_subst_emb0
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_App ?s; chop (subst ?\<rho> ?s) \<noteq> subst ?\<rho> (chop ?s)\<rbrakk> \<Longrightarrow> emb_step_at (replicate (num_args (fun ?s)) dir.Left) dir.Right (chop (subst ?\<rho> ?s)) = subst ?\<rho> (chop ?s)

goal (1 subgoal):
 1. chop (subst \<rho> s) \<unrhd>\<^sub>e\<^sub>m\<^sub>b subst \<rho> (chop s)
[PROOF STEP]
by (metis assms emb.refl emb_step_equiv emb_step_is_emb)


[STATEMENT]
lemma chop_subst_Hd:
  assumes "is_App s"
  assumes "is_Hd (subst \<rho> (Hd (head s)))"
  shows "chop (subst \<rho> s) = subst \<rho> (chop s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chop (subst \<rho> s) = subst \<rho> (chop s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. chop (subst \<rho> s) = subst \<rho> (chop s)
[PROOF STEP]
have "is_App (subst \<rho> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_App (subst \<rho> s)
[PROOF STEP]
by (metis assms(1) subst.simps(2) tm.collapse(2) tm.disc(2))
[PROOF STATE]
proof (state)
this:
is_App (subst \<rho> s)

goal (1 subgoal):
 1. chop (subst \<rho> s) = subst \<rho> (chop s)
[PROOF STEP]
have "num_args (fun s) = num_args (fun (subst \<rho> s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_args (fun s) = num_args (fun (subst \<rho> s))
[PROOF STEP]
unfolding fun_subst[OF \<open>is_App s\<close>,symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_args (fun s) = num_args (subst \<rho> (fun s))
[PROOF STEP]
using args_subst_Hd
[PROOF STATE]
proof (prove)
using this:
is_Hd (subst ?\<rho> (Hd (head ?s))) \<Longrightarrow> args (subst ?\<rho> ?s) = map (subst ?\<rho>) (args ?s)

goal (1 subgoal):
 1. num_args (fun s) = num_args (subst \<rho> (fun s))
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
is_Hd (subst ?\<rho> (Hd (head ?s))) \<Longrightarrow> args (subst ?\<rho> ?s) = map (subst ?\<rho>) (args ?s)
is_Hd (subst \<rho> (Hd (head s)))

goal (1 subgoal):
 1. num_args (fun s) = num_args (subst \<rho> (fun s))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
num_args (fun s) = num_args (fun (subst \<rho> s))

goal (1 subgoal):
 1. chop (subst \<rho> s) = subst \<rho> (chop s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
num_args (fun s) = num_args (fun (subst \<rho> s))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
num_args (fun s) = num_args (fun (subst \<rho> s))

goal (1 subgoal):
 1. chop (subst \<rho> s) = subst \<rho> (chop s)
[PROOF STEP]
unfolding chop_emb_step_at[OF assms(1)] chop_emb_step_at[OF \<open>is_App (subst \<rho> s)\<close>]
[PROOF STATE]
proof (prove)
using this:
num_args (fun s) = num_args (fun (subst \<rho> s))

goal (1 subgoal):
 1. emb_step_at (replicate (num_args (fun (subst \<rho> s))) dir.Left) dir.Right (subst \<rho> s) = subst \<rho> (emb_step_at (replicate (num_args (fun s)) dir.Left) dir.Right s)
[PROOF STEP]
using emb_step_at_subst[OF chop_position_of[OF \<open>is_App s\<close>]]
[PROOF STATE]
proof (prove)
using this:
num_args (fun s) = num_args (fun (subst \<rho> s))
emb_step_at (replicate (num_args (fun s)) dir.Left) dir.Right (subst ?\<rho> s) = subst ?\<rho> (emb_step_at (replicate (num_args (fun s)) dir.Left) dir.Right s)

goal (1 subgoal):
 1. emb_step_at (replicate (num_args (fun (subst \<rho> s))) dir.Left) dir.Right (subst \<rho> s) = subst \<rho> (emb_step_at (replicate (num_args (fun s)) dir.Left) dir.Right s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
chop (subst \<rho> s) = subst \<rho> (chop s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reflect_tranclp:
  assumes refl_f: "\<And>x y. S (f x) (f y) \<Longrightarrow> R x y"
  assumes bij_f: "bij_on_trancl S f"
  assumes prem: "S\<^sup>+\<^sup>+ (f x) (f y)"
  shows "R\<^sup>+\<^sup>+ x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R\<^sup>+\<^sup>+ x y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R\<^sup>+\<^sup>+ x y
[PROOF STEP]
define B where B: "B = range f"
[PROOF STATE]
proof (state)
this:
B = range f

goal (1 subgoal):
 1. R\<^sup>+\<^sup>+ x y
[PROOF STEP]
define g where g: "g = the_inv_into UNIV f"
[PROOF STATE]
proof (state)
this:
g = the_inv f

goal (1 subgoal):
 1. R\<^sup>+\<^sup>+ x y
[PROOF STEP]
define gr where gr: "gr = restrict g B"
[PROOF STATE]
proof (state)
this:
gr = restrict g B

goal (1 subgoal):
 1. R\<^sup>+\<^sup>+ x y
[PROOF STEP]
define P where P: "P = (\<lambda>x y. x \<in> B \<longrightarrow> y \<in> B \<longrightarrow> R\<^sup>+\<^sup>+ (gr x) (gr y))"
[PROOF STATE]
proof (state)
this:
P = (\<lambda>x y. x \<in> B \<longrightarrow> y \<in> B \<longrightarrow> R\<^sup>+\<^sup>+ (gr x) (gr y))

goal (1 subgoal):
 1. R\<^sup>+\<^sup>+ x y
[PROOF STEP]
from prem
[PROOF STATE]
proof (chain)
picking this:
S\<^sup>+\<^sup>+ (f x) (f y)
[PROOF STEP]
have major: "S\<^sup>+\<^sup>+ (f x) (f y)"
[PROOF STATE]
proof (prove)
using this:
S\<^sup>+\<^sup>+ (f x) (f y)

goal (1 subgoal):
 1. S\<^sup>+\<^sup>+ (f x) (f y)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S\<^sup>+\<^sup>+ (f x) (f y)

goal (1 subgoal):
 1. R\<^sup>+\<^sup>+ x y
[PROOF STEP]
from refl_f bij_f
[PROOF STATE]
proof (chain)
picking this:
S (f ?x) (f ?y) \<Longrightarrow> R ?x ?y
bij_on_trancl S f
[PROOF STEP]
have cases_1: "\<And>x y. S x y \<Longrightarrow> P x y"
[PROOF STATE]
proof (prove)
using this:
S (f ?x) (f ?y) \<Longrightarrow> R ?x ?y
bij_on_trancl S f

goal (1 subgoal):
 1. \<And>x y. S x y \<Longrightarrow> P x y
[PROOF STEP]
unfolding B P g gr
[PROOF STATE]
proof (prove)
using this:
S (f ?x) (f ?y) \<Longrightarrow> R ?x ?y
bij_on_trancl S f

goal (1 subgoal):
 1. \<And>x y. S x y \<Longrightarrow> x \<in> range f \<longrightarrow> y \<in> range f \<longrightarrow> R\<^sup>+\<^sup>+ (restrict (the_inv f) (range f) x) (restrict (the_inv f) (range f) y)
[PROOF STEP]
by (simp add: f_the_inv_into_f tranclp.r_into_trancl)
[PROOF STATE]
proof (state)
this:
S ?x ?y \<Longrightarrow> P ?x ?y

goal (1 subgoal):
 1. R\<^sup>+\<^sup>+ x y
[PROOF STEP]
from refl_f bij_f
[PROOF STATE]
proof (chain)
picking this:
S (f ?x) (f ?y) \<Longrightarrow> R ?x ?y
bij_on_trancl S f
[PROOF STEP]
have "(\<And>x y z. S\<^sup>+\<^sup>+ x y \<Longrightarrow> S\<^sup>+\<^sup>+ y z \<Longrightarrow> x \<in> B \<Longrightarrow> z \<in> B \<Longrightarrow> y \<in> B)"
[PROOF STATE]
proof (prove)
using this:
S (f ?x) (f ?y) \<Longrightarrow> R ?x ?y
bij_on_trancl S f

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>S\<^sup>+\<^sup>+ x y; S\<^sup>+\<^sup>+ y z; x \<in> B; z \<in> B\<rbrakk> \<Longrightarrow> y \<in> B
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
using this:
S (f ?x) (f ?y) \<Longrightarrow> R ?x ?y
bij_on_trancl S f

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>S\<^sup>+\<^sup>+ x y; S\<^sup>+\<^sup>+ y z; x \<in> range f; z \<in> range f\<rbrakk> \<Longrightarrow> y \<in> range f
[PROOF STEP]
by (rule_tac ?z="z" in tranclp_tranclp_to_tranclp_r, auto, blast)
[PROOF STATE]
proof (state)
this:
\<lbrakk>S\<^sup>+\<^sup>+ ?x ?y; S\<^sup>+\<^sup>+ ?y ?z; ?x \<in> B; ?z \<in> B\<rbrakk> \<Longrightarrow> ?y \<in> B

goal (1 subgoal):
 1. R\<^sup>+\<^sup>+ x y
[PROOF STEP]
with P
[PROOF STATE]
proof (chain)
picking this:
P = (\<lambda>x y. x \<in> B \<longrightarrow> y \<in> B \<longrightarrow> R\<^sup>+\<^sup>+ (gr x) (gr y))
\<lbrakk>S\<^sup>+\<^sup>+ ?x ?y; S\<^sup>+\<^sup>+ ?y ?z; ?x \<in> B; ?z \<in> B\<rbrakk> \<Longrightarrow> ?y \<in> B
[PROOF STEP]
have cases_2:
    "\<And>x y z. S\<^sup>+\<^sup>+ x y \<Longrightarrow> P x y \<Longrightarrow> S\<^sup>+\<^sup>+ y z \<Longrightarrow> P y z \<Longrightarrow> P x z"
[PROOF STATE]
proof (prove)
using this:
P = (\<lambda>x y. x \<in> B \<longrightarrow> y \<in> B \<longrightarrow> R\<^sup>+\<^sup>+ (gr x) (gr y))
\<lbrakk>S\<^sup>+\<^sup>+ ?x ?y; S\<^sup>+\<^sup>+ ?y ?z; ?x \<in> B; ?z \<in> B\<rbrakk> \<Longrightarrow> ?y \<in> B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>S\<^sup>+\<^sup>+ x y; P x y; S\<^sup>+\<^sup>+ y z; P y z\<rbrakk> \<Longrightarrow> P x z
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
using this:
P = (\<lambda>x y. x \<in> range f \<longrightarrow> y \<in> range f \<longrightarrow> R\<^sup>+\<^sup>+ (gr x) (gr y))
\<lbrakk>S\<^sup>+\<^sup>+ ?x ?y; S\<^sup>+\<^sup>+ ?y ?z; ?x \<in> range f; ?z \<in> range f\<rbrakk> \<Longrightarrow> ?y \<in> range f

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>S\<^sup>+\<^sup>+ x y; P x y; S\<^sup>+\<^sup>+ y z; P y z\<rbrakk> \<Longrightarrow> P x z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>S\<^sup>+\<^sup>+ ?x ?y; P ?x ?y; S\<^sup>+\<^sup>+ ?y ?z; P ?y ?z\<rbrakk> \<Longrightarrow> P ?x ?z

goal (1 subgoal):
 1. R\<^sup>+\<^sup>+ x y
[PROOF STEP]
from major cases_1 cases_2
[PROOF STATE]
proof (chain)
picking this:
S\<^sup>+\<^sup>+ (f x) (f y)
S ?x ?y \<Longrightarrow> P ?x ?y
\<lbrakk>S\<^sup>+\<^sup>+ ?x ?y; P ?x ?y; S\<^sup>+\<^sup>+ ?y ?z; P ?y ?z\<rbrakk> \<Longrightarrow> P ?x ?z
[PROOF STEP]
have "P (f x) (f y)"
[PROOF STATE]
proof (prove)
using this:
S\<^sup>+\<^sup>+ (f x) (f y)
S ?x ?y \<Longrightarrow> P ?x ?y
\<lbrakk>S\<^sup>+\<^sup>+ ?x ?y; P ?x ?y; S\<^sup>+\<^sup>+ ?y ?z; P ?y ?z\<rbrakk> \<Longrightarrow> P ?x ?z

goal (1 subgoal):
 1. P (f x) (f y)
[PROOF STEP]
by (rule tranclp_trans_induct)
[PROOF STATE]
proof (state)
this:
P (f x) (f y)

goal (1 subgoal):
 1. R\<^sup>+\<^sup>+ x y
[PROOF STEP]
with bij_f
[PROOF STATE]
proof (chain)
picking this:
bij_on_trancl S f
P (f x) (f y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bij_on_trancl S f
P (f x) (f y)

goal (1 subgoal):
 1. R\<^sup>+\<^sup>+ x y
[PROOF STEP]
unfolding P B g gr
[PROOF STATE]
proof (prove)
using this:
bij_on_trancl S f
f x \<in> range f \<longrightarrow> f y \<in> range f \<longrightarrow> R\<^sup>+\<^sup>+ (restrict (the_inv f) (range f) (f x)) (restrict (the_inv f) (range f) (f y))

goal (1 subgoal):
 1. R\<^sup>+\<^sup>+ x y
[PROOF STEP]
by (simp add: the_inv_f_f)
[PROOF STATE]
proof (state)
this:
R\<^sup>+\<^sup>+ x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_on_arev[intro!]: "inj_on arev S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on arev S
[PROOF STEP]
by (metis arev_arev inj_on_inverseI)


[STATEMENT]
lemma "\<exists>sinvar. \<not> sinvar G nP \<and> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>sinvar. \<not> sinvar G nP \<and> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP = {}
[PROOF STEP]
apply(simp add: SecurityInvariant_withOffendingFlows.set_offending_flows_def
    SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def SecurityInvariant_withOffendingFlows.is_offending_flows_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>sinvar. \<not> sinvar G nP \<and> (\<forall>x. sinvar (delete_edges G x) nP \<longrightarrow> x \<subseteq> edges G \<longrightarrow> sinvar G nP \<or> (\<exists>xa\<in>x. \<not> (case xa of (e1, e2) \<Rightarrow> \<not> sinvar (add_edge e1 e2 (delete_edges G x)) nP)))
[PROOF STEP]
apply(rule_tac x="(\<lambda>_ _. False)" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> False \<and> (\<forall>x. False \<longrightarrow> x \<subseteq> edges G \<longrightarrow> False \<or> (\<exists>x\<in>x. \<not> (case x of (e1, e2) \<Rightarrow> \<not> False)))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma psubstInp_preserves_good[simp]:
assumes good_rho: "goodEnv rho" and good: "goodInp inp"
shows "goodInp (inp %[rho])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. goodInp inp %[rho]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
goodEnv rho
goodInp inp

goal (1 subgoal):
 1. goodInp inp %[rho]
[PROOF STEP]
unfolding goodInp_def psubstInp_def liftAll_def
[PROOF STATE]
proof (prove)
using this:
goodEnv rho
(\<forall>i v. inp i = Some v \<longrightarrow> good v) \<and> |{i. inp i \<noteq> None}| <o |UNIV|

goal (1 subgoal):
 1. (\<forall>i v. lift (psubst rho) inp i = Some v \<longrightarrow> good v) \<and> |{i. lift (psubst rho) inp i \<noteq> None}| <o |UNIV|
[PROOF STEP]
by (auto simp add: lift_def split: option.splits)


[STATEMENT]
lemma skel_swap:
assumes "good X"
shows "skel (X #[x1 \<and> x2]_xs) = skel X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. skel (X #[x1 \<and> x2]_xs) = skel X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
good X

goal (1 subgoal):
 1. skel (X #[x1 \<and> x2]_xs) = skel X
[PROOF STEP]
by (metis alpha_qSkel pick_swap_qSwap qSkel_qSwap skel_def)


[STATEMENT]
lemma vydra_sound:
  assumes "reaches (run_vydra run_hd) (init_vydra init_hd run_hd \<phi>) n v" "run_vydra run_hd v = Some (v', (t, b))" "bounded_future_fmla \<phi>" "wf_fmla \<phi>"
  shows "(t, b) = (\<tau> \<sigma> n, sat \<phi> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t, b) = (\<tau> \<sigma> n, sat \<phi> n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (t, b) = (\<tau> \<sigma> n, sat \<phi> n)
[PROOF STEP]
have fst_v: "fst v = msize_fmla \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst v = msize_fmla \<phi>
[PROOF STEP]
by (rule reaches_invar[OF assms(1)]) (auto simp: init_vydra_def run_vydra_def Let_def)
[PROOF STATE]
proof (state)
this:
fst v = msize_fmla \<phi>

goal (1 subgoal):
 1. (t, b) = (\<tau> \<sigma> n, sat \<phi> n)
[PROOF STEP]
have "reaches (ru' \<phi>) (su' \<phi>) n (snd v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reaches (ru' \<phi>) (su' \<phi>) n (snd v)
[PROOF STEP]
using reaches_cong[OF assms(1), where ?P="\<lambda>(m, w). m = msize_fmla \<phi>" and ?g=snd]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>case init_vydra init_hd run_hd \<phi> of (m, w) \<Rightarrow> m = msize_fmla \<phi>; \<And>z z' v. \<lbrakk>case z of (m, w) \<Rightarrow> m = msize_fmla \<phi>; run_vydra run_hd z = Some (z', v)\<rbrakk> \<Longrightarrow> case z' of (m, w) \<Rightarrow> m = msize_fmla \<phi>; \<And>z. case z of (m, w) \<Rightarrow> m = msize_fmla \<phi> \<Longrightarrow> ?f' (snd z) = map_option (apfst snd) (run_vydra run_hd z)\<rbrakk> \<Longrightarrow> reaches ?f' (snd (init_vydra init_hd run_hd \<phi>)) n (snd v)

goal (1 subgoal):
 1. reaches (ru' \<phi>) (su' \<phi>) n (snd v)
[PROOF STEP]
by (auto simp: init_vydra_def run_vydra_def ru'_def su'_def map_option_apfst_idle Let_def simp del: sub.simps)
[PROOF STATE]
proof (state)
this:
reaches (ru' \<phi>) (su' \<phi>) n (snd v)

goal (1 subgoal):
 1. (t, b) = (\<tau> \<sigma> n, sat \<phi> n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
reaches (ru' \<phi>) (su' \<phi>) n (snd v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
reaches (ru' \<phi>) (su' \<phi>) n (snd v)

goal (1 subgoal):
 1. (t, b) = (\<tau> \<sigma> n, sat \<phi> n)
[PROOF STEP]
using vydra_sound'[OF _ _ assms(3,4)] assms(2) fst_v
[PROOF STATE]
proof (prove)
using this:
reaches (ru' \<phi>) (su' \<phi>) n (snd v)
\<lbrakk>reaches (ru' \<phi>) (su' \<phi>) ?n ?v; ru' \<phi> ?v = Some (?v', ?t, ?b)\<rbrakk> \<Longrightarrow> (?t, ?b) = (\<tau> \<sigma> ?n, sat \<phi> ?n)
run_vydra run_hd v = Some (v', t, b)
fst v = msize_fmla \<phi>

goal (1 subgoal):
 1. (t, b) = (\<tau> \<sigma> n, sat \<phi> n)
[PROOF STEP]
by (auto simp: run_vydra_def ru'_def split: prod.splits)
[PROOF STATE]
proof (state)
this:
(t, b) = (\<tau> \<sigma> n, sat \<phi> n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f1_less_f1': "f1 < f1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1 < f1'
[PROOF STEP]
using f1f2e
[PROOF STATE]
proof (prove)
using this:
f1 < f2 / e

goal (1 subgoal):
 1. f1 < f1'
[PROOF STEP]
by(auto simp add: f1'_def field_simps)


[STATEMENT]
lemma compress_normalize_protocols_step_not_introduces_Prot:
    "\<not> has_disc is_Prot m \<Longrightarrow> normalized_nnf_match m \<Longrightarrow> compress_normalize_protocols_step m = Some m' \<Longrightarrow>
     \<not> has_disc is_Prot m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> has_disc is_Prot m; normalized_nnf_match m; compress_normalize_protocols_step m = Some m'\<rbrakk> \<Longrightarrow> \<not> has_disc is_Prot m'
[PROOF STEP]
apply(simp add: compress_normalize_protocols_step_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> has_disc is_Prot m; normalized_nnf_match m; compress_normalize_primitive (is_Prot, prot_sel) Prot compress_protocols m = Some m'\<rbrakk> \<Longrightarrow> \<not> has_disc is_Prot m'
[PROOF STEP]
apply(drule compress_normalize_primitive_not_introduces_C[where m=m and C'=Prot])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>normalized_nnf_match m; compress_normalize_primitive (is_Prot, prot_sel) Prot compress_protocols m = Some m'\<rbrakk> \<Longrightarrow> wf_disc_sel (is_Prot, ?sel) Prot
 2. \<lbrakk>normalized_nnf_match m; compress_normalize_primitive (is_Prot, prot_sel) Prot compress_protocols m = Some m'\<rbrakk> \<Longrightarrow> normalized_nnf_match m
 3. \<lbrakk>normalized_nnf_match m; compress_normalize_primitive (is_Prot, prot_sel) Prot compress_protocols m = Some m'\<rbrakk> \<Longrightarrow> compress_normalize_primitive (is_Prot, ?sel) ?C ?f m = Some ?m'
 4. \<And>as_pos as_neg. \<lbrakk>normalized_nnf_match m; compress_normalize_primitive (is_Prot, prot_sel) Prot compress_protocols m = Some m'; ?f [] = Some (as_pos, as_neg)\<rbrakk> \<Longrightarrow> as_pos = [] \<and> as_neg = []
 5. \<lbrakk>normalized_nnf_match m; compress_normalize_primitive (is_Prot, prot_sel) Prot compress_protocols m = Some m'; \<not> has_disc is_Prot ?m'\<rbrakk> \<Longrightarrow> \<not> has_disc is_Prot m'
[PROOF STEP]
apply(simp_all add: wf_disc_sel_common_primitive(7))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as_pos as_neg. \<lbrakk>normalized_nnf_match m; compress_normalize_primitive (is_Prot, prot_sel) Prot compress_protocols m = Some m'; compress_protocols [] = Some (as_pos, as_neg)\<rbrakk> \<Longrightarrow> as_pos = [] \<and> as_neg = []
[PROOF STEP]
apply(simp add: compress_protocols_def split: if_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Exit_no_postdominator:
  "(_Exit_) postdominates n \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (_Exit_) postdominates n \<Longrightarrow> False
[PROOF STEP]
by(fastforce dest:Exit_path simp:postdominate_def)


[STATEMENT]
lemma diagonal_imp_upper_triangular:
  assumes "diagonal_mat A"
  and "A \<in> carrier_mat n n"
  shows "upper_triangular A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular A
[PROOF STEP]
unfolding  upper_triangular_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<dim_row A. \<forall>j<i. A $$ (i, j) = (0::'a)
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A; j < i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A; j < i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
assume "i < dim_row A" and "j < i"
[PROOF STATE]
proof (state)
this:
i < dim_row A
j < i

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A; j < i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
hence "j < dim_col A" "j \<noteq> i"
[PROOF STATE]
proof (prove)
using this:
i < dim_row A
j < i

goal (1 subgoal):
 1. j < dim_col A &&& j \<noteq> i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < dim_row A
j < i
diagonal_mat A
A \<in> carrier_mat n n

goal (1 subgoal):
 1. j < dim_col A &&& j \<noteq> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < dim_col A
j \<noteq> i

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A; j < i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
thus "A $$ (i,j) = 0"
[PROOF STATE]
proof (prove)
using this:
j < dim_col A
j \<noteq> i

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
using assms \<open>i < dim_row A\<close>
[PROOF STATE]
proof (prove)
using this:
j < dim_col A
j \<noteq> i
diagonal_mat A
A \<in> carrier_mat n n
i < dim_row A

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
unfolding diagonal_mat_def
[PROOF STATE]
proof (prove)
using this:
j < dim_col A
j \<noteq> i
\<forall>i<dim_row A. \<forall>j<dim_col A. i \<noteq> j \<longrightarrow> A $$ (i, j) = (0::'a)
A \<in> carrier_mat n n
i < dim_row A

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A $$ (i, j) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bv_mapzip_Nil [simp]: "bv_mapzip f [] [] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bv_mapzip f [] [] = []
[PROOF STEP]
by (simp add: bv_mapzip_def Let_def)


[STATEMENT]
lemma comp_elim:
"(P ;; Q) ac \<Longrightarrow> (\<And>a b c. ac = (a, c) \<Longrightarrow> P (a, b) \<Longrightarrow> Q (b, c) \<Longrightarrow> C) \<Longrightarrow> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P ;; Q) ac; \<And>a b c. \<lbrakk>ac = (a, c); P (a, b); Q (b, c)\<rbrakk> \<Longrightarrow> C\<rbrakk> \<Longrightarrow> C
[PROOF STEP]
by (auto simp add: comp_def)


[STATEMENT]
lemma eeqExcPID_N_eeq[simp,intro!]: "eeqExcPID_N s s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eeqExcPID_N s s
[PROOF STEP]
unfolding eeqExcPID_N_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>pid. if pid = PID then eqExcD (s pid) (s pid) else s pid = s pid
[PROOF STEP]
by auto


[STATEMENT]
lemma all_vars_for_consts_sub_consts:
  \<open>list_all (closed (length cs)) G \<Longrightarrow> list_all (\<lambda>c. list_all (new c) G) cs \<Longrightarrow> distinct cs \<Longrightarrow>
   map (\<lambda>p. vars_for_consts p cs) (map (sub_consts cs) G) = G\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all (closed (length cs)) G; list_all (\<lambda>c. news c G) cs; distinct cs\<rbrakk> \<Longrightarrow> map (\<lambda>p. vars_for_consts p cs) (map (sub_consts cs) G) = G
[PROOF STEP]
using vars_for_consts_sub_consts
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>closed (length ?cs) ?p; list_all (\<lambda>c. new c ?p) ?cs; distinct ?cs\<rbrakk> \<Longrightarrow> vars_for_consts (sub_consts ?cs ?p) ?cs = ?p

goal (1 subgoal):
 1. \<lbrakk>list_all (closed (length cs)) G; list_all (\<lambda>c. news c G) cs; distinct cs\<rbrakk> \<Longrightarrow> map (\<lambda>p. vars_for_consts p cs) (map (sub_consts cs) G) = G
[PROOF STEP]
unfolding list_all_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>closed (length ?cs) ?p; \<forall>c\<in>set ?cs. new c ?p; distinct ?cs\<rbrakk> \<Longrightarrow> vars_for_consts (sub_consts ?cs ?p) ?cs = ?p

goal (1 subgoal):
 1. \<lbrakk>Ball (set G) (closed (length cs)); \<forall>c\<in>set cs. \<forall>p\<in>set G. new c p; distinct cs\<rbrakk> \<Longrightarrow> map (\<lambda>p. vars_for_consts p cs) (map (sub_consts cs) G) = G
[PROOF STEP]
by (induct G) fastforce+


[STATEMENT]
lemma sub_consts_Neg: \<open>sub_consts cs (Neg p) = Neg (sub_consts cs p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_consts cs (Neg p) = Neg (sub_consts cs p)
[PROOF STEP]
by (induct cs arbitrary: p) simp_all


[STATEMENT]
lemma matrix_sum_distrib_left:
  fixes f :: "nat \<Rightarrow> complex mat"
  shows "P \<in> carrier_mat d d \<Longrightarrow> (\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d) \<Longrightarrow> matrix_sum d (\<lambda>k. P * (f k)) n = P * (matrix_sum d f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>P \<in> carrier_mat d d; \<And>k. k < 0 \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) 0 = P * matrix_sum d f 0
 2. \<And>n. \<lbrakk>\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n; P \<in> carrier_mat d d; \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat d d
?k < 0 \<Longrightarrow> f ?k \<in> carrier_mat d d

goal (2 subgoals):
 1. \<lbrakk>P \<in> carrier_mat d d; \<And>k. k < 0 \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) 0 = P * matrix_sum d f 0
 2. \<And>n. \<lbrakk>\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n; P \<in> carrier_mat d d; \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. P * f k) 0 = P * matrix_sum d f 0
[PROOF STEP]
unfolding matrix_sum.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>m d d = P * 0\<^sub>m d d
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier_mat d d
?k < 0 \<Longrightarrow> f ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. 0\<^sub>m d d = P * 0\<^sub>m d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. P * f k) 0 = P * matrix_sum d f 0

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n; P \<in> carrier_mat d d; \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n; P \<in> carrier_mat d d; \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n
P \<in> carrier_mat d d
?k < Suc n \<Longrightarrow> f ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n; P \<in> carrier_mat d d; \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n
P \<in> carrier_mat d d
?k < Suc n \<Longrightarrow> f ?k \<in> carrier_mat d d
[PROOF STEP]
have "\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n
P \<in> carrier_mat d d
?k < Suc n \<Longrightarrow> f ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> f ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n; P \<in> carrier_mat d d; \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> f ?k \<in> carrier_mat d d
[PROOF STEP]
have ds: "matrix_sum d f n \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> f ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d f n \<in> carrier_mat d d
[PROOF STEP]
using matrix_sum_dim
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> f ?k \<in> carrier_mat d d
(\<And>k. k < ?n \<Longrightarrow> ?f k \<in> carrier_mat ?d ?d) \<Longrightarrow> matrix_sum ?d ?f ?n \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. matrix_sum d f n \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d f n \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n; P \<in> carrier_mat d d; \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matrix_sum d f n \<in> carrier_mat d d
[PROOF STEP]
have dPf: "\<And>k. k < n \<Longrightarrow> P * f k \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
matrix_sum d f n \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> P * f k \<in> carrier_mat d d
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
matrix_sum d f n \<in> carrier_mat d d
\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n
P \<in> carrier_mat d d
?k < Suc n \<Longrightarrow> f ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> P * f k \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> P * f ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n; P \<in> carrier_mat d d; \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> P * f ?k \<in> carrier_mat d d
[PROOF STEP]
have "matrix_sum d (\<lambda>k. P * f k) n \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> P * f ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. P * f k) n \<in> carrier_mat d d
[PROOF STEP]
using matrix_sum_dim[OF dPf]
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> P * f ?k \<in> carrier_mat d d
(\<And>k. k < ?n \<Longrightarrow> ?k1 k < n) \<Longrightarrow> matrix_sum d (\<lambda>k. P * f (?k1 k)) ?n \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. P * f k) n \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. P * f k) n \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n; P \<in> carrier_mat d d; \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
have "matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * f n + matrix_sum d (\<lambda>k. P * f k) n "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * f n + matrix_sum d (\<lambda>k. P * f k) n
[PROOF STEP]
unfolding matrix_sum.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * f n + matrix_sum d (\<lambda>k. P * f k) n = P * f n + matrix_sum d (\<lambda>k. P * f k) n
[PROOF STEP]
using Suc(2)
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier_mat d d

goal (1 subgoal):
 1. P * f n + matrix_sum d (\<lambda>k. P * f k) n = P * f n + matrix_sum d (\<lambda>k. P * f k) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * f n + matrix_sum d (\<lambda>k. P * f k) n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n; P \<in> carrier_mat d d; \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * f n + matrix_sum d (\<lambda>k. P * f k) n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n; P \<in> carrier_mat d d; \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
have "\<dots> = P * f n + P * matrix_sum d f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * f n + matrix_sum d (\<lambda>k. P * f k) n = P * f n + P * matrix_sum d f n
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n
P \<in> carrier_mat d d
?k < Suc n \<Longrightarrow> f ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. P * f n + matrix_sum d (\<lambda>k. P * f k) n = P * f n + P * matrix_sum d f n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P * f n + matrix_sum d (\<lambda>k. P * f k) n = P * f n + P * matrix_sum d f n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n; P \<in> carrier_mat d d; \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
P * f n + matrix_sum d (\<lambda>k. P * f k) n = P * f n + P * matrix_sum d f n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n; P \<in> carrier_mat d d; \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
have "\<dots> = P * (f n + matrix_sum d f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * f n + P * matrix_sum d f n = P * (f n + matrix_sum d f n)
[PROOF STEP]
apply (mat_assoc d)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. matrix_sum d f n \<in> carrier_mat d d
 2. f n \<in> carrier_mat d d
 3. P \<in> carrier_mat d d
[PROOF STEP]
using ds dPf Suc
[PROOF STATE]
proof (prove)
using this:
matrix_sum d f n \<in> carrier_mat d d
?k < n \<Longrightarrow> P * f ?k \<in> carrier_mat d d
\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n
P \<in> carrier_mat d d
?k < Suc n \<Longrightarrow> f ?k \<in> carrier_mat d d

goal (3 subgoals):
 1. matrix_sum d f n \<in> carrier_mat d d
 2. f n \<in> carrier_mat d d
 3. P \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P * f n + P * matrix_sum d f n = P * (f n + matrix_sum d f n)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>P \<in> carrier_mat d d; \<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) n = P * matrix_sum d f n; P \<in> carrier_mat d d; \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * (f n + matrix_sum d f n)
[PROOF STEP]
show "matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * (matrix_sum d f (Suc n))"
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * (f n + matrix_sum d f n)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. P * f k) (Suc n) = P * matrix_sum d f (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma all_ctxt_closed_srstep_conversions [simp]:
  "all_ctxt_closed \<F> ((srstep \<F> \<R>)\<^sup>\<leftrightarrow>\<^sup>*)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_ctxt_closed \<F> ((srstep \<F> \<R>)\<^sup>\<leftrightarrow>\<^sup>*)
[PROOF STEP]
by (simp add: all_ctxt_closed_sig_rsteps sig_step_conversion_dist)


[STATEMENT]
lemma monC: "Der_1b \<D> \<Longrightarrow> MONO \<C>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Der_1b \<D> \<Longrightarrow> MONO \<C>
[PROOF STEP]
by (simp add: CD1b MONO_ADDIb)


[STATEMENT]
lemma vsubst_preserves_fresh:
assumes "good X"
and "fresh zs z X" and "zs \<noteq> ys \<or> z \<noteq> y1"
shows "fresh zs z (X #[y1 // y]_ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fresh zs z (X #[y1 // y]_ys)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
good X
fresh zs z X
zs \<noteq> ys \<or> z \<noteq> y1

goal (1 subgoal):
 1. fresh zs z (X #[y1 // y]_ys)
[PROOF STEP]
by(simp add: fresh_vsubst)


[STATEMENT]
lemma sdistinct_infinite_sset:
    assumes "sdistinct w"
    shows "infinite (sset w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (sset w)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sdistinct w

goal (1 subgoal):
 1. infinite (sset w)
[PROOF STEP]
by (coinduction arbitrary: w) (force elim: sdistinct.cases)


[STATEMENT]
lemma not_sdistinct_decomp:
    assumes "\<not> sdistinct w"
    obtains u v a w'
    where "w = u @- a ## v @- a ## w'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u a v w'. w = u @- a ## v @- a ## w' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>u a v w'. w = u @- a ## v @- a ## w' \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume 1: "\<not> thesis"
[PROOF STATE]
proof (state)
this:
\<not> thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>u a v w'. w = u @- a ## v @- a ## w' \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume 2: "w = u @- a ## v @- a ## w' \<Longrightarrow> thesis" for u a v w'
[PROOF STATE]
proof (state)
this:
w = ?u @- ?a ## ?v @- ?a ## ?w' \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>u a v w'. w = u @- a ## v @- a ## w' \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have 3: "\<forall> u v a w'. w \<noteq> u @- a ## v @- a ## w'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u v a w'. w \<noteq> u @- a ## v @- a ## w'
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
\<not> thesis
w = ?u @- ?a ## ?v @- ?a ## ?w' \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<forall>u v a w'. w \<noteq> u @- a ## v @- a ## w'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>u v a w'. w \<noteq> u @- a ## v @- a ## w'

goal (1 subgoal):
 1. \<lbrakk>\<And>u a v w'. w = u @- a ## v @- a ## w' \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have 4: "sdistinct w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdistinct w
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
\<forall>u v a w'. w \<noteq> u @- a ## v @- a ## w'

goal (1 subgoal):
 1. sdistinct w
[PROOF STEP]
by (coinduct) (metis id_stake_snth_sdrop imageE shift.simps sset_range)
[PROOF STATE]
proof (state)
this:
sdistinct w

goal (1 subgoal):
 1. \<lbrakk>\<And>u a v w'. w = u @- a ## v @- a ## w' \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using assms 4
[PROOF STATE]
proof (prove)
using this:
\<not> sdistinct w
sdistinct w

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma qmpt_factor_compose:
  assumes "qmpt M1 T1"
          "qmpt.qmpt_factor M1 T1 proj1 M2 T2"
          "qmpt.qmpt_factor M2 T2 proj2 M3 T3"
  shows "qmpt.qmpt_factor M1 T1 (proj2 o proj1) M3 T3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qmpt.qmpt_factor M1 T1 (proj2 \<circ> proj1) M3 T3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qmpt.qmpt_factor M1 T1 (proj2 \<circ> proj1) M3 T3
[PROOF STEP]
have *: "proj1 \<in> quasi_measure_preserving M1 M2 \<Longrightarrow> AE x in M2. proj2 (T2 x) = T3 (proj2 x)
      \<Longrightarrow> (AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>proj1 \<in> quasi_measure_preserving M1 M2; AE x in M2. proj2 (T2 x) = T3 (proj2 x)\<rbrakk> \<Longrightarrow> AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>proj1 \<in> quasi_measure_preserving M1 M2; AE x in M2. proj2 (T2 x) = T3 (proj2 x)\<rbrakk> \<Longrightarrow> AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
assume "AE y in M2. proj2 (T2 y) = T3 (proj2 y)"
           "proj1 \<in> quasi_measure_preserving M1 M2"
[PROOF STATE]
proof (state)
this:
AE y in M2. proj2 (T2 y) = T3 (proj2 y)
proj1 \<in> quasi_measure_preserving M1 M2

goal (1 subgoal):
 1. \<lbrakk>proj1 \<in> quasi_measure_preserving M1 M2; AE x in M2. proj2 (T2 x) = T3 (proj2 x)\<rbrakk> \<Longrightarrow> AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE y in M2. proj2 (T2 y) = T3 (proj2 y)
proj1 \<in> quasi_measure_preserving M1 M2
[PROOF STEP]
have "AE x in M1. proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))"
[PROOF STATE]
proof (prove)
using this:
AE y in M2. proj2 (T2 y) = T3 (proj2 y)
proj1 \<in> quasi_measure_preserving M1 M2

goal (1 subgoal):
 1. AE x in M1. proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
using quasi_measure_preserving_AE
[PROOF STATE]
proof (prove)
using this:
AE y in M2. proj2 (T2 y) = T3 (proj2 y)
proj1 \<in> quasi_measure_preserving M1 M2
\<lbrakk>?f \<in> quasi_measure_preserving ?M ?N; almost_everywhere ?N ?P\<rbrakk> \<Longrightarrow> AE x in ?M. ?P (?f x)

goal (1 subgoal):
 1. AE x in M1. proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M1. proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))

goal (1 subgoal):
 1. \<lbrakk>proj1 \<in> quasi_measure_preserving M1 M2; AE x in M2. proj2 (T2 x) = T3 (proj2 x)\<rbrakk> \<Longrightarrow> AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AE x in M1. proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))

goal (1 subgoal):
 1. \<lbrakk>proj1 \<in> quasi_measure_preserving M1 M2; AE x in M2. proj2 (T2 x) = T3 (proj2 x)\<rbrakk> \<Longrightarrow> AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
AE x in M1. proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))

goal (1 subgoal):
 1. \<lbrakk>proj1 \<in> quasi_measure_preserving M1 M2; AE x in M2. proj2 (T2 x) = T3 (proj2 x)\<rbrakk> \<Longrightarrow> AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>proj1 \<in> quasi_measure_preserving M1 M2; AE x in M2. proj2 (T2 x) = T3 (proj2 x)\<rbrakk> \<Longrightarrow> AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
assume "proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))"
[PROOF STATE]
proof (state)
this:
proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))

goal (1 subgoal):
 1. \<lbrakk>proj1 \<in> quasi_measure_preserving M1 M2; AE x in M2. proj2 (T2 x) = T3 (proj2 x)\<rbrakk> \<Longrightarrow> AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
have "proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))"
[PROOF STATE]
proof (prove)
using this:
proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))

goal (1 subgoal):
 1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))

goal (1 subgoal):
 1. \<lbrakk>proj1 \<in> quasi_measure_preserving M1 M2; AE x in M2. proj2 (T2 x) = T3 (proj2 x)\<rbrakk> \<Longrightarrow> AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
proj2 (T2 (proj1 ?x2)) = T3 (proj2 (proj1 ?x2)) \<Longrightarrow> proj1 (T1 ?x2) = T2 (proj1 ?x2) \<longrightarrow> proj2 (T2 (proj1 ?x2)) = T3 (proj2 (proj1 ?x2))

goal (1 subgoal):
 1. \<lbrakk>proj1 \<in> quasi_measure_preserving M1 M2; AE x in M2. proj2 (T2 x) = T3 (proj2 x)\<rbrakk> \<Longrightarrow> AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AE x in M1. proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
proj2 (T2 (proj1 ?x2)) = T3 (proj2 (proj1 ?x2)) \<Longrightarrow> proj1 (T1 ?x2) = T2 (proj1 ?x2) \<longrightarrow> proj2 (T2 (proj1 ?x2)) = T3 (proj2 (proj1 ?x2))
[PROOF STEP]
show "AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))"
[PROOF STATE]
proof (prove)
using this:
AE x in M1. proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
proj2 (T2 (proj1 ?x2)) = T3 (proj2 (proj1 ?x2)) \<Longrightarrow> proj1 (T1 ?x2) = T2 (proj1 ?x2) \<longrightarrow> proj2 (T2 (proj1 ?x2)) = T3 (proj2 (proj1 ?x2))

goal (1 subgoal):
 1. AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>proj1 \<in> quasi_measure_preserving M1 M2; AE x in M2. proj2 (T2 x) = T3 (proj2 x)\<rbrakk> \<Longrightarrow> AE x in M1. proj1 (T1 x) = T2 (proj1 x) \<longrightarrow> proj2 (T2 (proj1 x)) = T3 (proj2 (proj1 x))

goal (1 subgoal):
 1. qmpt.qmpt_factor M1 T1 (proj2 \<circ> proj1) M3 T3
[PROOF STEP]
interpret I: qmpt M1 T1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qmpt M1 T1
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
qmpt M1 T1

goal (1 subgoal):
 1. qmpt M1 T1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I.qmpt_factor (proj2 \<circ> proj1) M3 T3
[PROOF STEP]
interpret J: qmpt M2 T2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qmpt M2 T2
[PROOF STEP]
using I.qmpt_factorE(3)[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
qmpt M2 T2

goal (1 subgoal):
 1. qmpt M2 T2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I.qmpt_factor (proj2 \<circ> proj1) M3 T3
[PROOF STEP]
show "I.qmpt_factor (proj2 o proj1) M3 T3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I.qmpt_factor (proj2 \<circ> proj1) M3 T3
[PROOF STEP]
apply (rule I.qmpt_factorI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. proj2 \<circ> proj1 \<in> quasi_measure_preserving M1 M3
 2. AE x in M1. (proj2 \<circ> proj1) (T1 x) = T3 ((proj2 \<circ> proj1) x)
 3. qmpt M3 T3
[PROOF STEP]
using I.qmpt_factorE[OF assms(2)] J.qmpt_factorE[OF assms(3)]
[PROOF STATE]
proof (prove)
using this:
proj1 \<in> quasi_measure_preserving M1 M2
AE x in M1. proj1 (T1 x) = T2 (proj1 x)
qmpt M2 T2
proj2 \<in> quasi_measure_preserving M2 M3
AE x in M2. proj2 (T2 x) = T3 (proj2 x)
qmpt M3 T3

goal (3 subgoals):
 1. proj2 \<circ> proj1 \<in> quasi_measure_preserving M1 M3
 2. AE x in M1. (proj2 \<circ> proj1) (T1 x) = T3 ((proj2 \<circ> proj1) x)
 3. qmpt M3 T3
[PROOF STEP]
by (auto simp add: quasi_measure_preserving_comp *)
[PROOF STATE]
proof (state)
this:
I.qmpt_factor (proj2 \<circ> proj1) M3 T3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in igb_fr_graph)  lasso_prpl_acc_run_iff: "Ex is_lasso_prpl \<longleftrightarrow> Ex is_acc_run"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ex is_lasso_prpl = Ex is_acc_run
[PROOF STEP]
using acc_run_lasso_prpl lasso_prpl_acc_run
[PROOF STATE]
proof (prove)
using this:
Ex is_acc_run \<Longrightarrow> Ex is_lasso_prpl
is_lasso_prpl (?pr, ?pl) \<Longrightarrow> is_acc_run (?pr \<frown> ?pl\<^sup>\<omega>)

goal (1 subgoal):
 1. Ex is_lasso_prpl = Ex is_acc_run
[PROOF STEP]
by auto


[STATEMENT]
lemma HF_eq:
  "\<lbrakk>AHI hf' = AHI hf; UHI hf' = UHI hf; HVF hf' = HVF hf\<rbrakk> \<Longrightarrow> hf' = (hf::('x, 'y)HF)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>AHI hf' = AHI hf; UHI hf' = UHI hf; HVF hf' = HVF hf\<rbrakk> \<Longrightarrow> hf' = hf
[PROOF STEP]
apply(cases hf', cases hf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>AHIa UHIa HVFa AHIaa UHIaa HVFaa. \<lbrakk>AHI hf' = AHI hf; UHI hf' = UHI hf; HVF hf' = HVF hf; hf' = \<lparr>AHI = AHIa, UHI = UHIa, HVF = HVFa\<rparr>; hf = \<lparr>AHI = AHIaa, UHI = UHIaa, HVF = HVFaa\<rparr>\<rbrakk> \<Longrightarrow> hf' = hf
[PROOF STEP]
by(auto elim: HF.cases)