[STATEMENT]
lemma four_block_diag_unitary:
  assumes "unitary U1"
  and "unitary U2"
shows "unitary
  (four_block_diag U1 U2)"
(is "unitary ?fU")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex_Matrix.unitary (four_block_diag U1 U2)
[PROOF STEP]
unfolding unitary_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. four_block_diag U1 U2 \<in> carrier_mat (dim_row (four_block_diag U1 U2)) (dim_row (four_block_diag U1 U2)) \<and> inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. four_block_diag U1 U2 \<in> carrier_mat (dim_row (four_block_diag U1 U2)) (dim_row (four_block_diag U1 U2))
 2. inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
show "?fU \<in> carrier_mat (dim_row ?fU) (dim_row ?fU)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. four_block_diag U1 U2 \<in> carrier_mat (dim_row (four_block_diag U1 U2)) (dim_row (four_block_diag U1 U2))
[PROOF STEP]
by (metis Complex_Matrix.unitary_def assms(1) assms(2)
        four_block_carrier_mat index_mat_four_block(2))
[PROOF STATE]
proof (state)
this:
four_block_diag U1 U2 \<in> carrier_mat (dim_row (four_block_diag U1 U2)) (dim_row (four_block_diag U1 U2))

goal (1 subgoal):
 1. inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
define n where "n = dim_row ?fU"
[PROOF STATE]
proof (state)
this:
n = dim_row (four_block_diag U1 U2)

goal (1 subgoal):
 1. inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
show "inverts_mat ?fU (Complex_Matrix.adjoint ?fU)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
have "(Complex_Matrix.adjoint ?fU) =
      (four_block_mat (Complex_Matrix.adjoint U1)
      (0\<^sub>m (dim_col U1) (dim_row U2))
      (0\<^sub>m (dim_col U2) (dim_row U1))
      (Complex_Matrix.adjoint U2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex_Matrix.adjoint (four_block_diag U1 U2) = four_block_mat (Complex_Matrix.adjoint U1) (0\<^sub>m (dim_col U1) (dim_row U2)) (0\<^sub>m (dim_col U2) (dim_row U1)) (Complex_Matrix.adjoint U2)
[PROOF STEP]
by (rule eq_matI,
          auto simp: four_block_mat_adjoint zero_adjoint adjoint_eval)
[PROOF STATE]
proof (state)
this:
Complex_Matrix.adjoint (four_block_diag U1 U2) = four_block_mat (Complex_Matrix.adjoint U1) (0\<^sub>m (dim_col U1) (dim_row U2)) (0\<^sub>m (dim_col U2) (dim_row U1)) (Complex_Matrix.adjoint U2)

goal (1 subgoal):
 1. inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
hence "?fU * (Complex_Matrix.adjoint ?fU) =
      ?fU * (four_block_diag (Complex_Matrix.adjoint U1)
      (Complex_Matrix.adjoint U2))"
[PROOF STATE]
proof (prove)
using this:
Complex_Matrix.adjoint (four_block_diag U1 U2) = four_block_mat (Complex_Matrix.adjoint U1) (0\<^sub>m (dim_col U1) (dim_row U2)) (0\<^sub>m (dim_col U2) (dim_row U1)) (Complex_Matrix.adjoint U2)

goal (1 subgoal):
 1. four_block_diag U1 U2 * Complex_Matrix.adjoint (four_block_diag U1 U2) = four_block_diag U1 U2 * four_block_diag (Complex_Matrix.adjoint U1) (Complex_Matrix.adjoint U2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
four_block_diag U1 U2 * Complex_Matrix.adjoint (four_block_diag U1 U2) = four_block_diag U1 U2 * four_block_diag (Complex_Matrix.adjoint U1) (Complex_Matrix.adjoint U2)

goal (1 subgoal):
 1. inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
four_block_diag U1 U2 * Complex_Matrix.adjoint (four_block_diag U1 U2) = four_block_diag U1 U2 * four_block_diag (Complex_Matrix.adjoint U1) (Complex_Matrix.adjoint U2)

goal (1 subgoal):
 1. inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
have "... = four_block_diag
      (U1 * (Complex_Matrix.adjoint U1))
      (U2 * (Complex_Matrix.adjoint U2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. four_block_diag U1 U2 * four_block_diag (Complex_Matrix.adjoint U1) (Complex_Matrix.adjoint U2) = four_block_diag (U1 * Complex_Matrix.adjoint U1) (U2 * Complex_Matrix.adjoint U2)
[PROOF STEP]
by (rule mult_four_block_diag, (auto simp add: assms))
[PROOF STATE]
proof (state)
this:
four_block_diag U1 U2 * four_block_diag (Complex_Matrix.adjoint U1) (Complex_Matrix.adjoint U2) = four_block_diag (U1 * Complex_Matrix.adjoint U1) (U2 * Complex_Matrix.adjoint U2)

goal (1 subgoal):
 1. inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
four_block_diag U1 U2 * four_block_diag (Complex_Matrix.adjoint U1) (Complex_Matrix.adjoint U2) = four_block_diag (U1 * Complex_Matrix.adjoint U1) (U2 * Complex_Matrix.adjoint U2)

goal (1 subgoal):
 1. inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
have "... = four_block_mat
      (1\<^sub>m (dim_row U1))
      (0\<^sub>m (dim_row U1)  (dim_row U2))
      (0\<^sub>m (dim_row U2)  (dim_row U1))
      (1\<^sub>m (dim_row U2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. four_block_diag (U1 * Complex_Matrix.adjoint U1) (U2 * Complex_Matrix.adjoint U2) = four_block_mat (1\<^sub>m (dim_row U1)) (0\<^sub>m (dim_row U1) (dim_row U2)) (0\<^sub>m (dim_row U2) (dim_row U1)) (1\<^sub>m (dim_row U2))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Complex_Matrix.unitary U1
Complex_Matrix.unitary U2

goal (1 subgoal):
 1. four_block_diag (U1 * Complex_Matrix.adjoint U1) (U2 * Complex_Matrix.adjoint U2) = four_block_mat (1\<^sub>m (dim_row U1)) (0\<^sub>m (dim_row U1) (dim_row U2)) (0\<^sub>m (dim_row U2) (dim_row U1)) (1\<^sub>m (dim_row U2))
[PROOF STEP]
unfolding unitary_def inverts_mat_def
[PROOF STATE]
proof (prove)
using this:
U1 \<in> carrier_mat (dim_row U1) (dim_row U1) \<and> U1 * Complex_Matrix.adjoint U1 = 1\<^sub>m (dim_row U1)
U2 \<in> carrier_mat (dim_row U2) (dim_row U2) \<and> U2 * Complex_Matrix.adjoint U2 = 1\<^sub>m (dim_row U2)

goal (1 subgoal):
 1. four_block_diag (U1 * Complex_Matrix.adjoint U1) (U2 * Complex_Matrix.adjoint U2) = four_block_mat (1\<^sub>m (dim_row U1)) (0\<^sub>m (dim_row U1) (dim_row U2)) (0\<^sub>m (dim_row U2) (dim_row U1)) (1\<^sub>m (dim_row U2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
four_block_diag (U1 * Complex_Matrix.adjoint U1) (U2 * Complex_Matrix.adjoint U2) = four_block_mat (1\<^sub>m (dim_row U1)) (0\<^sub>m (dim_row U1) (dim_row U2)) (0\<^sub>m (dim_row U2) (dim_row U1)) (1\<^sub>m (dim_row U2))

goal (1 subgoal):
 1. inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
four_block_diag (U1 * Complex_Matrix.adjoint U1) (U2 * Complex_Matrix.adjoint U2) = four_block_mat (1\<^sub>m (dim_row U1)) (0\<^sub>m (dim_row U1) (dim_row U2)) (0\<^sub>m (dim_row U2) (dim_row U1)) (1\<^sub>m (dim_row U2))

goal (1 subgoal):
 1. inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
have "... = 1\<^sub>m (dim_row U1 + dim_row U2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. four_block_mat (1\<^sub>m (dim_row U1)) (0\<^sub>m (dim_row U1) (dim_row U2)) (0\<^sub>m (dim_row U2) (dim_row U1)) (1\<^sub>m (dim_row U2)) = 1\<^sub>m (dim_row U1 + dim_row U2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
four_block_mat (1\<^sub>m (dim_row U1)) (0\<^sub>m (dim_row U1) (dim_row U2)) (0\<^sub>m (dim_row U2) (dim_row U1)) (1\<^sub>m (dim_row U2)) = 1\<^sub>m (dim_row U1 + dim_row U2)

goal (1 subgoal):
 1. inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
four_block_diag U1 U2 * Complex_Matrix.adjoint (four_block_diag U1 U2) = 1\<^sub>m (dim_row U1 + dim_row U2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
four_block_diag U1 U2 * Complex_Matrix.adjoint (four_block_diag U1 U2) = 1\<^sub>m (dim_row U1 + dim_row U2)

goal (1 subgoal):
 1. inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))
[PROOF STEP]
unfolding inverts_mat_def
[PROOF STATE]
proof (prove)
using this:
four_block_diag U1 U2 * Complex_Matrix.adjoint (four_block_diag U1 U2) = 1\<^sub>m (dim_row U1 + dim_row U2)

goal (1 subgoal):
 1. four_block_diag U1 U2 * Complex_Matrix.adjoint (four_block_diag U1 U2) = 1\<^sub>m (dim_row (four_block_diag U1 U2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inverts_mat (four_block_diag U1 U2) (Complex_Matrix.adjoint (four_block_diag U1 U2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma regular_comp:
  assumes f: "regular f"
  assumes g: "regular g"
  shows "regular (g o f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regular (g \<circ> f)
[PROOF STEP]
using continuous_comp f g regular_def setmonotone_comp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>continuous ?f; continuous ?g\<rbrakk> \<Longrightarrow> continuous (?g \<circ> ?f)
regular f
regular g
regular ?f = (setmonotone ?f \<and> continuous ?f)
\<lbrakk>setmonotone ?f; setmonotone ?g\<rbrakk> \<Longrightarrow> setmonotone (?g \<circ> ?f)

goal (1 subgoal):
 1. regular (g \<circ> f)
[PROOF STEP]
by blast


[STATEMENT]
lemma regular_limit: "regular f \<Longrightarrow> regular (limit f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regular f \<Longrightarrow> regular (limit f)
[PROOF STEP]
by (simp add: continuous_limit regular_def setmonotone_limit)


[STATEMENT]
lemma steps_ConsD:
  "steps xs" if "steps (x # xs)" "xs \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps xs
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
steps (x # xs)
xs \<noteq> []

goal (1 subgoal):
 1. steps xs
[PROOF STEP]
by (auto elim: steps.cases)


[STATEMENT]
lemma simulation_reaches1:
  "\<exists> b'. B\<^sup>+\<^sup>+ b b' \<and> a' \<sim> b'" if "A\<^sup>+\<^sup>+ a a'" "a \<sim> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b'. B.reaches1 b b' \<and> a' \<sim> b'
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
A.reaches1 a a'
a \<sim> b

goal (1 subgoal):
 1. \<exists>b'. B.reaches1 b b' \<and> a' \<sim> b'
[PROOF STEP]
by (induction rule: tranclp_induct) (auto 4 3 intro: tranclp.intros(2) dest: A_B_step)


[STATEMENT]
lemma 1[simp]: "distinct (map fst (ts1@ts2)) \<Longrightarrow>
    pr (\<alpha> (ts1@ts2)) x i = pr (\<alpha> ts1) x i + pr (\<alpha> ts2) x i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (ts1 @ ts2)) \<Longrightarrow> local.pr (\<alpha> (ts1 @ ts2)) x i = local.pr (\<alpha> ts1) x i + local.pr (\<alpha> ts2) x i
[PROOF STEP]
apply (auto simp: pr_def \<alpha>_def map_add_def aux split: option.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (map fst ts1); distinct (map fst ts2); fst ` set ts1 \<inter> fst ` set ts2 = {}\<rbrakk> \<Longrightarrow> (\<Sum>k = 0..<n. x k * (the_default 0 (map_of ts1 (k, i)) + the_default 0 (map_of ts2 (k, i)))) = (\<Sum>k = 0..<n. x k * the_default 0 (map_of ts1 (k, i))) + (\<Sum>k = 0..<n. x k * the_default 0 (map_of ts2 (k, i)))
[PROOF STEP]
apply (auto simp: algebra_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (map fst ts1); distinct (map fst ts2); fst ` set ts1 \<inter> fst ` set ts2 = {}\<rbrakk> \<Longrightarrow> (\<Sum>k = 0..<n. x k * the_default 0 (map_of ts1 (k, i)) + x k * the_default 0 (map_of ts2 (k, i))) = (\<Sum>k = 0..<n. x k * the_default 0 (map_of ts1 (k, i))) + (\<Sum>k = 0..<n. x k * the_default 0 (map_of ts2 (k, i)))
[PROOF STEP]
by (simp add: sum.distrib)


[STATEMENT]
lemma cindexP_rectpath_interior_base:
  assumes "r\<in>box a b"
  shows "cindexP_pathE [:-r,1:] (rectpath a b) = -2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindexP_pathE [:- r, 1:] (rectpath a b) = - 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cindexP_pathE [:- r, 1:] (rectpath a b) = - 2
[PROOF STEP]
have inbox:"Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}
[PROOF STEP]
using \<open>r\<in>box a b\<close>
[PROOF STATE]
proof (prove)
using this:
r \<in> box a b

goal (1 subgoal):
 1. Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}
[PROOF STEP]
unfolding in_box_complex_iff
[PROOF STATE]
proof (prove)
using this:
Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}

goal (1 subgoal):
 1. Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}

goal (1 subgoal):
 1. cindexP_pathE [:- r, 1:] (rectpath a b) = - 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}
[PROOF STEP]
have r_nzero:"r\<noteq>a" "r\<noteq>Complex (Re b) (Im a)" "r\<noteq>b" "r\<noteq>Complex (Re a) (Im b)"
[PROOF STATE]
proof (prove)
using this:
Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}

goal (1 subgoal):
 1. (r \<noteq> a &&& r \<noteq> Complex (Re b) (Im a)) &&& r \<noteq> b &&& r \<noteq> Complex (Re a) (Im b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<noteq> a
r \<noteq> Complex (Re b) (Im a)
r \<noteq> b
r \<noteq> Complex (Re a) (Im b)

goal (1 subgoal):
 1. cindexP_pathE [:- r, 1:] (rectpath a b) = - 2
[PROOF STEP]
have "Re a < Re b" "Im a < Im b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re a < Re b &&& Im a < Im b
[PROOF STEP]
using \<open>r\<in>box a b\<close> complex_box_ne_empty
[PROOF STATE]
proof (prove)
using this:
r \<in> box a b
(cbox ?a ?b \<noteq> {}) = (Re ?a \<le> Re ?b \<and> Im ?a \<le> Im ?b)
(box ?a ?b \<noteq> {}) = (Re ?a < Re ?b \<and> Im ?a < Im ?b)

goal (1 subgoal):
 1. Re a < Re b &&& Im a < Im b
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
Re a < Re b
Im a < Im b

goal (1 subgoal):
 1. cindexP_pathE [:- r, 1:] (rectpath a b) = - 2
[PROOF STEP]
define rr where "rr = [:-r,1:]"
[PROOF STATE]
proof (state)
this:
rr = [:- r, 1:]

goal (1 subgoal):
 1. cindexP_pathE [:- r, 1:] (rectpath a b) = - 2
[PROOF STEP]
have rr_linepath:"cindexP_pathE rr (linepath a b)
          = cindex_pathE (linepath (a - r) (b-r)) 0 " for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindexP_pathE rr (linepath a b) = cindex_pathE (linepath (a - r) (b - r)) 0
[PROOF STEP]
unfolding rr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindexP_pathE [:- r, 1:] (linepath a b) = cindex_pathE (linepath (a - r) (b - r)) 0
[PROOF STEP]
unfolding cindexP_lineE_def cindexP_pathE_def poly_linepath_comp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindex_pathE (poly ([:- r, 1:] \<circ>\<^sub>p [:a, b - a:]) \<circ> complex_of_real) 0 = cindex_pathE (linepath (a - r) (b - r)) 0
[PROOF STEP]
by (simp add:poly_pcompose comp_def linepath_def scaleR_conv_of_real algebra_simps)
[PROOF STATE]
proof (state)
this:
cindexP_pathE rr (linepath ?a ?b) = cindex_pathE (linepath (?a - r) (?b - r)) 0

goal (1 subgoal):
 1. cindexP_pathE [:- r, 1:] (rectpath a b) = - 2
[PROOF STEP]
have "cindexP_pathE rr (rectpath a b) =
                 cindexP_pathE rr (linepath a (Complex (Re b) (Im a)))
                 + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b)
                 + cindexP_pathE rr (linepath b (Complex (Re a) (Im b)))
                 + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindexP_pathE rr (rectpath a b) = cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a)
[PROOF STEP]
unfolding rectpath_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindexP_pathE rr (linepath a (Complex (Re b) (Im a)) +++ linepath (Complex (Re b) (Im a)) b +++ linepath b (Complex (Re a) (Im b)) +++ linepath (Complex (Re a) (Im b)) a) = cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a)
[PROOF STEP]
by ((subst cindex_poly_pathE_joinpaths
            |subst finite_ReZ_segments_joinpaths
            |intro path_poly_comp conjI);
        (simp add:poly_linepath_comp finite_ReZ_segments_poly_of_real path_compose_join
          pathfinish_compose pathstart_compose poly_pcompose)?)+
[PROOF STATE]
proof (state)
this:
cindexP_pathE rr (rectpath a b) = cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a)

goal (1 subgoal):
 1. cindexP_pathE [:- r, 1:] (rectpath a b) = - 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cindexP_pathE rr (rectpath a b) = cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a)

goal (1 subgoal):
 1. cindexP_pathE [:- r, 1:] (rectpath a b) = - 2
[PROOF STEP]
have "... = -2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = - 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = - 2
[PROOF STEP]
have "cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) = - 1
[PROOF STEP]
unfolding rr_linepath
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindex_pathE (linepath (a - r) (Complex (Re b) (Im a) - r)) 0 = - 1
[PROOF STEP]
apply (subst cindex_pathE_linepath)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<notin> closed_segment (a - r) (Complex (Re b) (Im a) - r)
 2. (let c1 = Re (a - r) - Re 0; c2 = Re (Complex (Re b) (Im a) - r) - Re 0; c3 = Im (a - r) * Re (Complex (Re b) (Im a) - r) + Re 0 * Im (Complex (Re b) (Im a) - r) + Im 0 * Re (a - r) - Im 0 * Re (Complex (Re b) (Im a) - r) - Im (Complex (Re b) (Im a) - r) * Re (a - r) - Re 0 * Im (a - r); d1 = Im (a - r) - Im 0; d2 = Im (Complex (Re b) (Im a) - r) - Im 0 in if 0 < c1 \<and> c2 < 0 \<or> c1 < 0 \<and> 0 < c2 then if 0 < c3 then 1 else - 1 else if (c1 = 0) = (c2 \<noteq> 0) \<and> (c1 = 0 \<longrightarrow> d1 \<noteq> 0) \<and> (c2 = 0 \<longrightarrow> d2 \<noteq> 0) then if c1 = 0 \<and> (0 < c2) = (0 < d1) \<or> c2 = 0 \<and> (0 < c1) = (d2 < 0) then 1 / 2 else - 1 / 2 else 0) = - 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> closed_segment (a - r) (Complex (Re b) (Im a) - r)
[PROOF STEP]
using closed_segment_imp_Re_Im(2) inbox
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> closed_segment ?lb ?ub; Im ?lb \<le> Im ?ub\<rbrakk> \<Longrightarrow> Im ?lb \<le> Im ?x \<and> Im ?x \<le> Im ?ub
Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}

goal (1 subgoal):
 1. 0 \<notin> closed_segment (a - r) (Complex (Re b) (Im a) - r)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let c1 = Re (a - r) - Re 0; c2 = Re (Complex (Re b) (Im a) - r) - Re 0; c3 = Im (a - r) * Re (Complex (Re b) (Im a) - r) + Re 0 * Im (Complex (Re b) (Im a) - r) + Im 0 * Re (a - r) - Im 0 * Re (Complex (Re b) (Im a) - r) - Im (Complex (Re b) (Im a) - r) * Re (a - r) - Re 0 * Im (a - r); d1 = Im (a - r) - Im 0; d2 = Im (Complex (Re b) (Im a) - r) - Im 0 in if 0 < c1 \<and> c2 < 0 \<or> c1 < 0 \<and> 0 < c2 then if 0 < c3 then 1 else - 1 else if (c1 = 0) = (c2 \<noteq> 0) \<and> (c1 = 0 \<longrightarrow> d1 \<noteq> 0) \<and> (c2 = 0 \<longrightarrow> d2 \<noteq> 0) then if c1 = 0 \<and> (0 < c2) = (0 < d1) \<or> c2 = 0 \<and> (0 < c1) = (d2 < 0) then 1 / 2 else - 1 / 2 else 0) = - 1
[PROOF STEP]
using inbox
[PROOF STATE]
proof (prove)
using this:
Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}

goal (1 subgoal):
 1. (let c1 = Re (a - r) - Re 0; c2 = Re (Complex (Re b) (Im a) - r) - Re 0; c3 = Im (a - r) * Re (Complex (Re b) (Im a) - r) + Re 0 * Im (Complex (Re b) (Im a) - r) + Im 0 * Re (a - r) - Im 0 * Re (Complex (Re b) (Im a) - r) - Im (Complex (Re b) (Im a) - r) * Re (a - r) - Re 0 * Im (a - r); d1 = Im (a - r) - Im 0; d2 = Im (Complex (Re b) (Im a) - r) - Im 0 in if 0 < c1 \<and> c2 < 0 \<or> c1 < 0 \<and> 0 < c2 then if 0 < c3 then 1 else - 1 else if (c1 = 0) = (c2 \<noteq> 0) \<and> (c1 = 0 \<longrightarrow> d1 \<noteq> 0) \<and> (c2 = 0 \<longrightarrow> d2 \<noteq> 0) then if c1 = 0 \<and> (0 < c2) = (0 < d1) \<or> c2 = 0 \<and> (0 < c1) = (d2 < 0) then 1 / 2 else - 1 / 2 else 0) = - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) = - 1

goal (1 subgoal):
 1. cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = - 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) = - 1

goal (1 subgoal):
 1. cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = - 2
[PROOF STEP]
have "cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) = 0
[PROOF STEP]
unfolding rr_linepath
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindex_pathE (linepath (Complex (Re b) (Im a) - r) (b - r)) 0 = 0
[PROOF STEP]
apply (subst cindex_pathE_linepath)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<notin> closed_segment (Complex (Re b) (Im a) - r) (b - r)
 2. (let c1 = Re (Complex (Re b) (Im a) - r) - Re 0; c2 = Re (b - r) - Re 0; c3 = Im (Complex (Re b) (Im a) - r) * Re (b - r) + Re 0 * Im (b - r) + Im 0 * Re (Complex (Re b) (Im a) - r) - Im 0 * Re (b - r) - Im (b - r) * Re (Complex (Re b) (Im a) - r) - Re 0 * Im (Complex (Re b) (Im a) - r); d1 = Im (Complex (Re b) (Im a) - r) - Im 0; d2 = Im (b - r) - Im 0 in if 0 < c1 \<and> c2 < 0 \<or> c1 < 0 \<and> 0 < c2 then if 0 < c3 then 1 else - 1 else if (c1 = 0) = (c2 \<noteq> 0) \<and> (c1 = 0 \<longrightarrow> d1 \<noteq> 0) \<and> (c2 = 0 \<longrightarrow> d2 \<noteq> 0) then if c1 = 0 \<and> (0 < c2) = (0 < d1) \<or> c2 = 0 \<and> (0 < c1) = (d2 < 0) then 1 / 2 else - 1 / 2 else 0) = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> closed_segment (Complex (Re b) (Im a) - r) (b - r)
[PROOF STEP]
using closed_segment_imp_Re_Im(1) inbox
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> closed_segment ?lb ?ub; Re ?lb \<le> Re ?ub\<rbrakk> \<Longrightarrow> Re ?lb \<le> Re ?x \<and> Re ?x \<le> Re ?ub
Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}

goal (1 subgoal):
 1. 0 \<notin> closed_segment (Complex (Re b) (Im a) - r) (b - r)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let c1 = Re (Complex (Re b) (Im a) - r) - Re 0; c2 = Re (b - r) - Re 0; c3 = Im (Complex (Re b) (Im a) - r) * Re (b - r) + Re 0 * Im (b - r) + Im 0 * Re (Complex (Re b) (Im a) - r) - Im 0 * Re (b - r) - Im (b - r) * Re (Complex (Re b) (Im a) - r) - Re 0 * Im (Complex (Re b) (Im a) - r); d1 = Im (Complex (Re b) (Im a) - r) - Im 0; d2 = Im (b - r) - Im 0 in if 0 < c1 \<and> c2 < 0 \<or> c1 < 0 \<and> 0 < c2 then if 0 < c3 then 1 else - 1 else if (c1 = 0) = (c2 \<noteq> 0) \<and> (c1 = 0 \<longrightarrow> d1 \<noteq> 0) \<and> (c2 = 0 \<longrightarrow> d2 \<noteq> 0) then if c1 = 0 \<and> (0 < c2) = (0 < d1) \<or> c2 = 0 \<and> (0 < c1) = (d2 < 0) then 1 / 2 else - 1 / 2 else 0) = 0
[PROOF STEP]
using inbox
[PROOF STATE]
proof (prove)
using this:
Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}

goal (1 subgoal):
 1. (let c1 = Re (Complex (Re b) (Im a) - r) - Re 0; c2 = Re (b - r) - Re 0; c3 = Im (Complex (Re b) (Im a) - r) * Re (b - r) + Re 0 * Im (b - r) + Im 0 * Re (Complex (Re b) (Im a) - r) - Im 0 * Re (b - r) - Im (b - r) * Re (Complex (Re b) (Im a) - r) - Re 0 * Im (Complex (Re b) (Im a) - r); d1 = Im (Complex (Re b) (Im a) - r) - Im 0; d2 = Im (b - r) - Im 0 in if 0 < c1 \<and> c2 < 0 \<or> c1 < 0 \<and> 0 < c2 then if 0 < c3 then 1 else - 1 else if (c1 = 0) = (c2 \<noteq> 0) \<and> (c1 = 0 \<longrightarrow> d1 \<noteq> 0) \<and> (c2 = 0 \<longrightarrow> d2 \<noteq> 0) then if c1 = 0 \<and> (0 < c2) = (0 < d1) \<or> c2 = 0 \<and> (0 < c1) = (d2 < 0) then 1 / 2 else - 1 / 2 else 0) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) = 0

goal (1 subgoal):
 1. cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = - 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) = 0

goal (1 subgoal):
 1. cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = - 2
[PROOF STEP]
have "cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) = - 1
[PROOF STEP]
unfolding rr_linepath
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindex_pathE (linepath (b - r) (Complex (Re a) (Im b) - r)) 0 = - 1
[PROOF STEP]
apply (subst cindex_pathE_linepath)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<notin> closed_segment (b - r) (Complex (Re a) (Im b) - r)
 2. (let c1 = Re (b - r) - Re 0; c2 = Re (Complex (Re a) (Im b) - r) - Re 0; c3 = Im (b - r) * Re (Complex (Re a) (Im b) - r) + Re 0 * Im (Complex (Re a) (Im b) - r) + Im 0 * Re (b - r) - Im 0 * Re (Complex (Re a) (Im b) - r) - Im (Complex (Re a) (Im b) - r) * Re (b - r) - Re 0 * Im (b - r); d1 = Im (b - r) - Im 0; d2 = Im (Complex (Re a) (Im b) - r) - Im 0 in if 0 < c1 \<and> c2 < 0 \<or> c1 < 0 \<and> 0 < c2 then if 0 < c3 then 1 else - 1 else if (c1 = 0) = (c2 \<noteq> 0) \<and> (c1 = 0 \<longrightarrow> d1 \<noteq> 0) \<and> (c2 = 0 \<longrightarrow> d2 \<noteq> 0) then if c1 = 0 \<and> (0 < c2) = (0 < d1) \<or> c2 = 0 \<and> (0 < c1) = (d2 < 0) then 1 / 2 else - 1 / 2 else 0) = - 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> closed_segment (b - r) (Complex (Re a) (Im b) - r)
[PROOF STEP]
using closed_segment_imp_Re_Im(2) inbox
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> closed_segment ?lb ?ub; Im ?lb \<le> Im ?ub\<rbrakk> \<Longrightarrow> Im ?lb \<le> Im ?x \<and> Im ?x \<le> Im ?ub
Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}

goal (1 subgoal):
 1. 0 \<notin> closed_segment (b - r) (Complex (Re a) (Im b) - r)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let c1 = Re (b - r) - Re 0; c2 = Re (Complex (Re a) (Im b) - r) - Re 0; c3 = Im (b - r) * Re (Complex (Re a) (Im b) - r) + Re 0 * Im (Complex (Re a) (Im b) - r) + Im 0 * Re (b - r) - Im 0 * Re (Complex (Re a) (Im b) - r) - Im (Complex (Re a) (Im b) - r) * Re (b - r) - Re 0 * Im (b - r); d1 = Im (b - r) - Im 0; d2 = Im (Complex (Re a) (Im b) - r) - Im 0 in if 0 < c1 \<and> c2 < 0 \<or> c1 < 0 \<and> 0 < c2 then if 0 < c3 then 1 else - 1 else if (c1 = 0) = (c2 \<noteq> 0) \<and> (c1 = 0 \<longrightarrow> d1 \<noteq> 0) \<and> (c2 = 0 \<longrightarrow> d2 \<noteq> 0) then if c1 = 0 \<and> (0 < c2) = (0 < d1) \<or> c2 = 0 \<and> (0 < c1) = (d2 < 0) then 1 / 2 else - 1 / 2 else 0) = - 1
[PROOF STEP]
using inbox
[PROOF STATE]
proof (prove)
using this:
Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}

goal (1 subgoal):
 1. (let c1 = Re (b - r) - Re 0; c2 = Re (Complex (Re a) (Im b) - r) - Re 0; c3 = Im (b - r) * Re (Complex (Re a) (Im b) - r) + Re 0 * Im (Complex (Re a) (Im b) - r) + Im 0 * Re (b - r) - Im 0 * Re (Complex (Re a) (Im b) - r) - Im (Complex (Re a) (Im b) - r) * Re (b - r) - Re 0 * Im (b - r); d1 = Im (b - r) - Im 0; d2 = Im (Complex (Re a) (Im b) - r) - Im 0 in if 0 < c1 \<and> c2 < 0 \<or> c1 < 0 \<and> 0 < c2 then if 0 < c3 then 1 else - 1 else if (c1 = 0) = (c2 \<noteq> 0) \<and> (c1 = 0 \<longrightarrow> d1 \<noteq> 0) \<and> (c2 = 0 \<longrightarrow> d2 \<noteq> 0) then if c1 = 0 \<and> (0 < c2) = (0 < d1) \<or> c2 = 0 \<and> (0 < c1) = (d2 < 0) then 1 / 2 else - 1 / 2 else 0) = - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) = - 1

goal (1 subgoal):
 1. cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = - 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) = - 1

goal (1 subgoal):
 1. cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = - 2
[PROOF STEP]
have "cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = 0
[PROOF STEP]
unfolding rr_linepath
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindex_pathE (linepath (Complex (Re a) (Im b) - r) (a - r)) 0 = 0
[PROOF STEP]
apply (subst cindex_pathE_linepath)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<notin> closed_segment (Complex (Re a) (Im b) - r) (a - r)
 2. (let c1 = Re (Complex (Re a) (Im b) - r) - Re 0; c2 = Re (a - r) - Re 0; c3 = Im (Complex (Re a) (Im b) - r) * Re (a - r) + Re 0 * Im (a - r) + Im 0 * Re (Complex (Re a) (Im b) - r) - Im 0 * Re (a - r) - Im (a - r) * Re (Complex (Re a) (Im b) - r) - Re 0 * Im (Complex (Re a) (Im b) - r); d1 = Im (Complex (Re a) (Im b) - r) - Im 0; d2 = Im (a - r) - Im 0 in if 0 < c1 \<and> c2 < 0 \<or> c1 < 0 \<and> 0 < c2 then if 0 < c3 then 1 else - 1 else if (c1 = 0) = (c2 \<noteq> 0) \<and> (c1 = 0 \<longrightarrow> d1 \<noteq> 0) \<and> (c2 = 0 \<longrightarrow> d2 \<noteq> 0) then if c1 = 0 \<and> (0 < c2) = (0 < d1) \<or> c2 = 0 \<and> (0 < c1) = (d2 < 0) then 1 / 2 else - 1 / 2 else 0) = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> closed_segment (Complex (Re a) (Im b) - r) (a - r)
[PROOF STEP]
using closed_segment_imp_Re_Im(1) inbox
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> closed_segment ?lb ?ub; Re ?lb \<le> Re ?ub\<rbrakk> \<Longrightarrow> Re ?lb \<le> Re ?x \<and> Re ?x \<le> Re ?ub
Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}

goal (1 subgoal):
 1. 0 \<notin> closed_segment (Complex (Re a) (Im b) - r) (a - r)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let c1 = Re (Complex (Re a) (Im b) - r) - Re 0; c2 = Re (a - r) - Re 0; c3 = Im (Complex (Re a) (Im b) - r) * Re (a - r) + Re 0 * Im (a - r) + Im 0 * Re (Complex (Re a) (Im b) - r) - Im 0 * Re (a - r) - Im (a - r) * Re (Complex (Re a) (Im b) - r) - Re 0 * Im (Complex (Re a) (Im b) - r); d1 = Im (Complex (Re a) (Im b) - r) - Im 0; d2 = Im (a - r) - Im 0 in if 0 < c1 \<and> c2 < 0 \<or> c1 < 0 \<and> 0 < c2 then if 0 < c3 then 1 else - 1 else if (c1 = 0) = (c2 \<noteq> 0) \<and> (c1 = 0 \<longrightarrow> d1 \<noteq> 0) \<and> (c2 = 0 \<longrightarrow> d2 \<noteq> 0) then if c1 = 0 \<and> (0 < c2) = (0 < d1) \<or> c2 = 0 \<and> (0 < c1) = (d2 < 0) then 1 / 2 else - 1 / 2 else 0) = 0
[PROOF STEP]
using inbox
[PROOF STATE]
proof (prove)
using this:
Re r \<in> {Re a<..<Re b} \<and> Im r \<in> {Im a<..<Im b}

goal (1 subgoal):
 1. (let c1 = Re (Complex (Re a) (Im b) - r) - Re 0; c2 = Re (a - r) - Re 0; c3 = Im (Complex (Re a) (Im b) - r) * Re (a - r) + Re 0 * Im (a - r) + Im 0 * Re (Complex (Re a) (Im b) - r) - Im 0 * Re (a - r) - Im (a - r) * Re (Complex (Re a) (Im b) - r) - Re 0 * Im (Complex (Re a) (Im b) - r); d1 = Im (Complex (Re a) (Im b) - r) - Im 0; d2 = Im (a - r) - Im 0 in if 0 < c1 \<and> c2 < 0 \<or> c1 < 0 \<and> 0 < c2 then if 0 < c3 then 1 else - 1 else if (c1 = 0) = (c2 \<noteq> 0) \<and> (c1 = 0 \<longrightarrow> d1 \<noteq> 0) \<and> (c2 = 0 \<longrightarrow> d2 \<noteq> 0) then if c1 = 0 \<and> (0 < c2) = (0 < d1) \<or> c2 = 0 \<and> (0 < c1) = (d2 < 0) then 1 / 2 else - 1 / 2 else 0) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = 0

goal (1 subgoal):
 1. cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = - 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) = - 1
cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) = 0
cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) = - 1
cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) = - 1
cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) = 0
cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) = - 1
cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = 0

goal (1 subgoal):
 1. cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = - 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = - 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cindexP_pathE rr (linepath a (Complex (Re b) (Im a))) + cindexP_pathE rr (linepath (Complex (Re b) (Im a)) b) + cindexP_pathE rr (linepath b (Complex (Re a) (Im b))) + cindexP_pathE rr (linepath (Complex (Re a) (Im b)) a) = - 2

goal (1 subgoal):
 1. cindexP_pathE [:- r, 1:] (rectpath a b) = - 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cindexP_pathE rr (rectpath a b) = - 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cindexP_pathE rr (rectpath a b) = - 2

goal (1 subgoal):
 1. cindexP_pathE [:- r, 1:] (rectpath a b) = - 2
[PROOF STEP]
unfolding rr_def
[PROOF STATE]
proof (prove)
using this:
cindexP_pathE [:- r, 1:] (rectpath a b) = - 2

goal (1 subgoal):
 1. cindexP_pathE [:- r, 1:] (rectpath a b) = - 2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cindexP_pathE [:- r, 1:] (rectpath a b) = - 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_iterator_sng_correct :
  "set_iterator (set_iterator_sng x) {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator (set_iterator_sng x) {x}
[PROOF STEP]
unfolding set_iterator_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_genord (set_iterator_sng x) {x} (\<lambda>_ _. True)
[PROOF STEP]
by (rule set_iterator_genord_sng_correct)


[STATEMENT]
lemma iADDIb_rel: "iADDI_b \<phi> = ADDI_b \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iADDI_b \<phi> = ADDI_b \<phi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iADDI_b \<phi> = ADDI_b \<phi>
[PROOF STEP]
have lr: "iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
[PROOF STEP]
assume iaddib: "iADDI_b \<phi>"
[PROOF STATE]
proof (state)
this:
iADDI_b \<phi>

goal (1 subgoal):
 1. iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
iADDI_b \<phi>

goal (1 subgoal):
 1. iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
[PROOF STEP]
fix A::"\<sigma>" and B::"\<sigma>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
[PROOF STEP]
let ?S="\<lambda>Z. Z=A \<or> Z=B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
[PROOF STEP]
from iaddib
[PROOF STATE]
proof (chain)
picking this:
iADDI_b \<phi>
[PROOF STEP]
have "\<phi>(\<^bold>\<Or>?S) \<^bold>\<succeq> \<^bold>\<exists>\<^sup>R\<lparr>?S\<rparr>(\<phi>)"
[PROOF STATE]
proof (prove)
using this:
iADDI_b \<phi>

goal (1 subgoal):
 1. contains (\<phi> \<^bold>\<Or>\<lambda>Z. Z = A \<or> Z = B) (\<lambda>w. nonEmpty (\<lambda>X. (X = A \<or> X = B) \<and> \<phi> X w))
[PROOF STEP]
by (simp add: iADDI_b_def Ra_restr_ex)
[PROOF STATE]
proof (state)
this:
contains (\<phi> \<^bold>\<Or>\<lambda>Z. Z = A \<or> Z = B) (\<lambda>w. nonEmpty (\<lambda>X. (X = A \<or> X = B) \<and> \<phi> X w))

goal (1 subgoal):
 1. iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
contains (\<phi> \<^bold>\<Or>\<lambda>Z. Z = A \<or> Z = B) (\<lambda>w. nonEmpty (\<lambda>X. (X = A \<or> X = B) \<and> \<phi> X w))

goal (1 subgoal):
 1. iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
[PROOF STEP]
have "\<^bold>\<Or>?S = A \<^bold>\<or> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<Or>\<lambda>Z. Z = A \<or> Z = B = A \<^bold>\<or> B
[PROOF STEP]
using supremum_def join_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<Or>?S \<equiv> \<lambda>w. nonEmpty (\<lambda>X. ?S X \<and> X w)
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w

goal (1 subgoal):
 1. \<^bold>\<Or>\<lambda>Z. Z = A \<or> Z = B = A \<^bold>\<or> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<^bold>\<Or>\<lambda>Z. Z = A \<or> Z = B = A \<^bold>\<or> B

goal (1 subgoal):
 1. iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<Or>\<lambda>Z. Z = A \<or> Z = B = A \<^bold>\<or> B

goal (1 subgoal):
 1. iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
[PROOF STEP]
have "\<^bold>\<exists>\<^sup>R\<lparr>?S\<rparr>(\<phi>) = (\<phi> A) \<^bold>\<or> (\<phi> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>w. nonEmpty (\<lambda>X. (X = A \<or> X = B) \<and> \<phi> X w)) = \<phi> A \<^bold>\<or> \<phi> B
[PROOF STEP]
using join_def
[PROOF STATE]
proof (prove)
using this:
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w

goal (1 subgoal):
 1. (\<lambda>w. nonEmpty (\<lambda>X. (X = A \<or> X = B) \<and> \<phi> X w)) = \<phi> A \<^bold>\<or> \<phi> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>w. nonEmpty (\<lambda>X. (X = A \<or> X = B) \<and> \<phi> X w)) = \<phi> A \<^bold>\<or> \<phi> B

goal (1 subgoal):
 1. iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
contains (\<phi> \<^bold>\<Or>\<lambda>Z. Z = A \<or> Z = B) (\<lambda>w. nonEmpty (\<lambda>X. (X = A \<or> X = B) \<and> \<phi> X w))
\<^bold>\<Or>\<lambda>Z. Z = A \<or> Z = B = A \<^bold>\<or> B
(\<lambda>w. nonEmpty (\<lambda>X. (X = A \<or> X = B) \<and> \<phi> X w)) = \<phi> A \<^bold>\<or> \<phi> B
[PROOF STEP]
have "\<phi>(A \<^bold>\<or> B) \<^bold>\<succeq> (\<phi> A) \<^bold>\<or> (\<phi> B)"
[PROOF STATE]
proof (prove)
using this:
contains (\<phi> \<^bold>\<Or>\<lambda>Z. Z = A \<or> Z = B) (\<lambda>w. nonEmpty (\<lambda>X. (X = A \<or> X = B) \<and> \<phi> X w))
\<^bold>\<Or>\<lambda>Z. Z = A \<or> Z = B = A \<^bold>\<or> B
(\<lambda>w. nonEmpty (\<lambda>X. (X = A \<or> X = B) \<and> \<phi> X w)) = \<phi> A \<^bold>\<or> \<phi> B

goal (1 subgoal):
 1. contains (\<phi> (A \<^bold>\<or> B)) (\<phi> A \<^bold>\<or> \<phi> B)
[PROOF STEP]
by smt
[PROOF STATE]
proof (state)
this:
contains (\<phi> (A \<^bold>\<or> B)) (\<phi> A \<^bold>\<or> \<phi> B)

goal (1 subgoal):
 1. iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
contains (\<phi> (?A2 \<^bold>\<or> ?B2)) (\<phi> ?A2 \<^bold>\<or> \<phi> ?B2)

goal (1 subgoal):
 1. iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
contains (\<phi> (?A2 \<^bold>\<or> ?B2)) (\<phi> ?A2 \<^bold>\<or> \<phi> ?B2)

goal (1 subgoal):
 1. ADDI_b \<phi>
[PROOF STEP]
by (simp add: ADDI_b_def)
[PROOF STATE]
proof (state)
this:
ADDI_b \<phi>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>

goal (1 subgoal):
 1. iADDI_b \<phi> = ADDI_b \<phi>
[PROOF STEP]
have rl: "ADDI_b \<phi> \<Longrightarrow> iADDI_b \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ADDI_b \<phi> \<Longrightarrow> iADDI_b \<phi>
[PROOF STEP]
by (smt MONO_def MONO_ADDIb Ra_restr_ex iADDI_b_def sup_char)
[PROOF STATE]
proof (state)
this:
ADDI_b \<phi> \<Longrightarrow> iADDI_b \<phi>

goal (1 subgoal):
 1. iADDI_b \<phi> = ADDI_b \<phi>
[PROOF STEP]
from lr rl
[PROOF STATE]
proof (chain)
picking this:
iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
ADDI_b \<phi> \<Longrightarrow> iADDI_b \<phi>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
iADDI_b \<phi> \<Longrightarrow> ADDI_b \<phi>
ADDI_b \<phi> \<Longrightarrow> iADDI_b \<phi>

goal (1 subgoal):
 1. iADDI_b \<phi> = ADDI_b \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
iADDI_b \<phi> = ADDI_b \<phi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma esing_eqvt[eqvt]: "\<pi> \<bullet> (esing x) = esing (\<pi> \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> esing x = esing (\<pi> \<bullet> x)
[PROOF STEP]
unfolding esing_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> (\<Lambda> a. (\<lambda>y. if x = y then a else \<bottom>)) = (\<Lambda> a. (\<lambda>y. if \<pi> \<bullet> x = y then a else \<bottom>))
[PROOF STEP]
apply perm_simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<bullet> Abs_cfun) (\<lambda>xa xb. if \<pi> \<bullet> x = xb then xa else \<bottom>) = (\<Lambda> a. (\<lambda>y. if \<pi> \<bullet> x = y then a else \<bottom>))
[PROOF STEP]
apply (simp add: Abs_cfun_eqvt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gState_progress_refl[simp,intro!]:
  "gState_inv prog g \<Longrightarrow> (g,g) \<in> (gState_progress_rel prog)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gState_inv prog g \<Longrightarrow> (g, g) \<in> gState_progress_rel prog
[PROOF STEP]
unfolding gState_progress_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gState_inv prog g \<Longrightarrow> (g, g) \<in> {(g, g'). gState_inv prog g \<and> gState_inv prog g' \<and> length (gState.channels g) \<le> length (gState.channels g') \<and> dom (lm.\<alpha> (gState.vars g)) = dom (lm.\<alpha> (gState.vars g'))}
[PROOF STEP]
by auto


[STATEMENT]
lemma eval_peval: \<open>eval h (g o lift) p = peval h g (lift p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval h (g \<circ> lift) p = peval h g (lift p)
[PROOF STEP]
by (induct p) simp_all


[STATEMENT]
lemma eq_\<I>_gpv_map_gpv2: "eq_\<I>_gpv A \<I> gpv (map_gpv f id gpv') = eq_\<I>_gpv (\<lambda>x y. A x (f y)) \<I> gpv gpv'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_\<I>_gpv A \<I> gpv (map_gpv f id gpv') = eq_\<I>_gpv (\<lambda>x y. A x (f y)) \<I> gpv gpv'
[PROOF STEP]
using eq_\<I>_gpv_map_gpv1[of "conversep A" \<I> f gpv' gpv]
[PROOF STATE]
proof (prove)
using this:
eq_\<I>_gpv A\<inverse>\<inverse> \<I> (map_gpv f id gpv') gpv = eq_\<I>_gpv (\<lambda>x. A\<inverse>\<inverse> (f x)) \<I> gpv' gpv

goal (1 subgoal):
 1. eq_\<I>_gpv A \<I> gpv (map_gpv f id gpv') = eq_\<I>_gpv (\<lambda>x y. A x (f y)) \<I> gpv gpv'
[PROOF STEP]
by(rewrite in "_ = \<hole>" conversep_iff[symmetric] , simp add: eq_\<I>_gpv_conversep[symmetric])
    (subst (asm) eq_\<I>_gpv_conversep , simp add: conversep_iff[abs_def])


[STATEMENT]
lemma sublist_nth: \<open>\<lbrakk>lo \<le> hi; hi < length xs; k+lo \<le> hi\<rbrakk> \<Longrightarrow> (sublist xs lo hi)!k = xs!(lo+k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lo \<le> hi; hi < length xs; k + lo \<le> hi\<rbrakk> \<Longrightarrow> WB_Sort.sublist xs lo hi ! k = xs ! (lo + k)
[PROOF STEP]
by (simp add: sublist_def)


[STATEMENT]
lemma t2n_mask_eq_if:
  "2 ^ n AND mask m = (if n < m then 2 ^ n else (0 :: 'a::len word))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ n AND mask m = (if n < m then 2 ^ n else 0)
[PROOF STEP]
by word_eqI_solve


[STATEMENT]
lemma btree_insert_to_fun [hoare_triple]:
  "<btree t b>
   btree_insert k v b
   <btree (tree_insert k v t)>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <btree t b> btree_insert k v b <btree (tree_insert k v t)>
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <btree t b> btree_insert k v b <btree (tree_insert k v t)>
[PROOF STEP]
@induct t arbitrary b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <btree t b> btree_insert k v b <btree (tree_insert k v t)>
[PROOF STEP]
@qed


[STATEMENT]
lemma foo2: "\<lbrakk>eqExcRLR rl rl'; \<not> isRevRoleFor PID x\<rbrakk> \<Longrightarrow> eqExcRLR (List.insert x rl) (List.insert x rl')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eqExcRLR rl rl'; \<not> isRevRoleFor PID x\<rbrakk> \<Longrightarrow> eqExcRLR (List.insert x rl) (List.insert x rl')
[PROOF STEP]
unfolding eqExcRLR_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>filter (\<lambda>r. \<not> isRevRoleFor PID r) rl = filter (\<lambda>r. \<not> isRevRoleFor PID r) rl'; \<not> isRevRoleFor PID x\<rbrakk> \<Longrightarrow> filter (\<lambda>r. \<not> isRevRoleFor PID r) (List.insert x rl) = filter (\<lambda>r. \<not> isRevRoleFor PID r) (List.insert x rl')
[PROOF STEP]
apply (auto simp: foo1) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>filter (\<lambda>r. \<not> isRevRoleFor PID r) rl = filter (\<lambda>r. \<not> isRevRoleFor PID r) rl'; \<not> isRevRoleFor PID x; x \<in>\<in> rl\<rbrakk> \<Longrightarrow> x \<in>\<in> rl'
 2. \<lbrakk>filter (\<lambda>r. \<not> isRevRoleFor PID r) rl = filter (\<lambda>r. \<not> isRevRoleFor PID r) rl'; \<not> isRevRoleFor PID x; x \<notin> set rl; x \<in>\<in> rl'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis eqExcRLR_def eqExcRLR_set isRevRoleFor.simps)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hom_deltas: "hom_ab (fold delta_a w br) = fold delta_b w (hom_ab br)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hom_ab (fold delta_a w br) = fold delta_b w (hom_ab br)
[PROOF STEP]
by (induct w arbitrary: br) (auto simp add: hom_delta)


[STATEMENT]
lemma f2'_pos: "eventually (\<lambda>x. f2' x > 0) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. 0 < f2' x
[PROOF STEP]
proof (subst eventually_at_top_linorder, intro exI allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. ?N \<le> n \<Longrightarrow> 0 < f2' n
[PROOF STEP]
fix x :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. ?N \<le> n \<Longrightarrow> 0 < f2' n
[PROOF STEP]
assume "x \<ge> gx0"
[PROOF STATE]
proof (state)
this:
gx0 \<le> x

goal (1 subgoal):
 1. \<And>n. ?N \<le> n \<Longrightarrow> 0 < f2' n
[PROOF STEP]
thus "f2' x > 0"
[PROOF STATE]
proof (prove)
using this:
gx0 \<le> x

goal (1 subgoal):
 1. 0 < f2' x
[PROOF STEP]
proof (induction x rule: f2'.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x < gx1; gx0 \<le> x\<rbrakk> \<Longrightarrow> 0 < f2' x
 2. \<And>x. \<lbrakk>gx1 \<le> x; \<And>xa. \<lbrakk>xa \<in> {..<k}; gx0 \<le> (ts ! xa) x\<rbrakk> \<Longrightarrow> 0 < f2' ((ts ! xa) x); gx0 \<le> x\<rbrakk> \<Longrightarrow> 0 < f2' x
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:
x < gx1
gx0 \<le> x

goal (2 subgoals):
 1. \<And>x. \<lbrakk>x < gx1; gx0 \<le> x\<rbrakk> \<Longrightarrow> 0 < f2' x
 2. \<And>x. \<lbrakk>gx1 \<le> x; \<And>xa. \<lbrakk>xa \<in> {..<k}; gx0 \<le> (ts ! xa) x\<rbrakk> \<Longrightarrow> 0 < f2' ((ts ! xa) x); gx0 \<le> x\<rbrakk> \<Longrightarrow> 0 < f2' x
[PROOF STEP]
with gc2 gx0(2)[of x]
[PROOF STATE]
proof (chain)
picking this:
0 < gc2
\<forall>\<^sub>F x in sequentially. gc2 * g' (real x) \<le> g x
gx0 \<le> x \<Longrightarrow> 0 < f x
x < gx1
gx0 \<le> x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 < gc2
\<forall>\<^sub>F x in sequentially. gc2 * g' (real x) \<le> g x
gx0 \<le> x \<Longrightarrow> 0 < f x
x < gx1
gx0 \<le> x

goal (1 subgoal):
 1. 0 < f2' x
[PROOF STEP]
by (simp add: max_def field_simps)
[PROOF STATE]
proof (state)
this:
0 < f2' x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>gx1 \<le> x; \<And>xa. \<lbrakk>xa \<in> {..<k}; gx0 \<le> (ts ! xa) x\<rbrakk> \<Longrightarrow> 0 < f2' ((ts ! xa) x); gx0 \<le> x\<rbrakk> \<Longrightarrow> 0 < f2' x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>gx1 \<le> x; \<And>xa. \<lbrakk>xa \<in> {..<k}; gx0 \<le> (ts ! xa) x\<rbrakk> \<Longrightarrow> 0 < f2' ((ts ! xa) x); gx0 \<le> x\<rbrakk> \<Longrightarrow> 0 < f2' x
[PROOF STEP]
case prems: (2 x)
[PROOF STATE]
proof (state)
this:
gx1 \<le> x
\<lbrakk>?xa \<in> {..<k}; gx0 \<le> (ts ! ?xa) x\<rbrakk> \<Longrightarrow> 0 < f2' ((ts ! ?xa) x)
gx0 \<le> x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>gx1 \<le> x; \<And>xa. \<lbrakk>xa \<in> {..<k}; gx0 \<le> (ts ! xa) x\<rbrakk> \<Longrightarrow> 0 < f2' ((ts ! xa) x); gx0 \<le> x\<rbrakk> \<Longrightarrow> 0 < f2' x
[PROOF STEP]
have "(\<Sum>i<k. as!i*f2' ((ts!i) x)) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (\<Sum>i<k. as ! i * f2' ((ts ! i) x))
[PROOF STEP]
proof (rule sum_pos')
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. finite {..<k}
 2. \<exists>x\<in>{..<k}. 0 < as ! x * f2' ((ts ! x) x)
 3. \<And>x. x \<in> {..<k} \<Longrightarrow> 0 \<le> as ! x * f2' ((ts ! x) x)
[PROOF STEP]
from ex_pos_a'
[PROOF STATE]
proof (chain)
picking this:
\<exists>i<k. 0 < as ! i
[PROOF STEP]
guess i
[PROOF STATE]
proof (prove)
using this:
\<exists>i<k. 0 < as ! i

goal (1 subgoal):
 1. thesis
goal instantiation:
PROP ?guess \<leadsto> thesis
[PROOF STEP]
by (elim exE conjE)
[PROOF STATE]
proof (state)
this:
i < k
0 < as ! i

goal (3 subgoals):
 1. finite {..<k}
 2. \<exists>x\<in>{..<k}. 0 < as ! x * f2' ((ts ! x) x)
 3. \<And>x. x \<in> {..<k} \<Longrightarrow> 0 \<le> as ! x * f2' ((ts ! x) x)
[PROOF STEP]
note i = this
[PROOF STATE]
proof (state)
this:
i < k
0 < as ! i

goal (3 subgoals):
 1. finite {..<k}
 2. \<exists>x\<in>{..<k}. 0 < as ! x * f2' ((ts ! x) x)
 3. \<And>x. x \<in> {..<k} \<Longrightarrow> 0 \<le> as ! x * f2' ((ts ! x) x)
[PROOF STEP]
with prems(1) gx0 gx1
[PROOF STATE]
proof (chain)
picking this:
gx1 \<le> x
gx0 \<le> ?x \<Longrightarrow> gc2 * g' (real ?x) \<le> g ?x
gx0 \<le> ?x \<Longrightarrow> 0 < f ?x
gx0 \<le> ?x \<Longrightarrow> 0 \<le> g' (real ?x)
\<lbrakk>gx1 \<le> ?x; ?i < k\<rbrakk> \<Longrightarrow> gx0 \<le> (ts ! ?i) ?x
i < k
0 < as ! i
[PROOF STEP]
have "as!i * f2' ((ts!i) x) > 0"
[PROOF STATE]
proof (prove)
using this:
gx1 \<le> x
gx0 \<le> ?x \<Longrightarrow> gc2 * g' (real ?x) \<le> g ?x
gx0 \<le> ?x \<Longrightarrow> 0 < f ?x
gx0 \<le> ?x \<Longrightarrow> 0 \<le> g' (real ?x)
\<lbrakk>gx1 \<le> ?x; ?i < k\<rbrakk> \<Longrightarrow> gx0 \<le> (ts ! ?i) ?x
i < k
0 < as ! i

goal (1 subgoal):
 1. 0 < as ! i * f2' ((ts ! i) x)
[PROOF STEP]
by (intro mult_pos_pos prems(2)) simp_all
[PROOF STATE]
proof (state)
this:
0 < as ! i * f2' ((ts ! i) x)

goal (3 subgoals):
 1. finite {..<k}
 2. \<exists>x\<in>{..<k}. 0 < as ! x * f2' ((ts ! x) x)
 3. \<And>x. x \<in> {..<k} \<Longrightarrow> 0 \<le> as ! x * f2' ((ts ! x) x)
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
i < k
0 < as ! i
0 < as ! i * f2' ((ts ! i) x)
[PROOF STEP]
show "\<exists>i\<in>{..<k}. as!i * f2' ((ts!i) x) > 0"
[PROOF STATE]
proof (prove)
using this:
i < k
0 < as ! i
0 < as ! i * f2' ((ts ! i) x)

goal (1 subgoal):
 1. \<exists>i\<in>{..<k}. 0 < as ! i * f2' ((ts ! i) x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>{..<k}. 0 < as ! i * f2' ((ts ! i) x)

goal (2 subgoals):
 1. finite {..<k}
 2. \<And>x. x \<in> {..<k} \<Longrightarrow> 0 \<le> as ! x * f2' ((ts ! x) x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite {..<k}
 2. \<And>x. x \<in> {..<k} \<Longrightarrow> 0 \<le> as ! x * f2' ((ts ! x) x)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite {..<k}
 2. \<And>x. x \<in> {..<k} \<Longrightarrow> 0 \<le> as ! x * f2' ((ts ! x) x)
[PROOF STEP]
assume i: "i \<in> {..<k}"
[PROOF STATE]
proof (state)
this:
i \<in> {..<k}

goal (2 subgoals):
 1. finite {..<k}
 2. \<And>x. x \<in> {..<k} \<Longrightarrow> 0 \<le> as ! x * f2' ((ts ! x) x)
[PROOF STEP]
with prems(1)
[PROOF STATE]
proof (chain)
picking this:
gx1 \<le> x
i \<in> {..<k}
[PROOF STEP]
have "f2' ((ts!i) x) > 0"
[PROOF STATE]
proof (prove)
using this:
gx1 \<le> x
i \<in> {..<k}

goal (1 subgoal):
 1. 0 < f2' ((ts ! i) x)
[PROOF STEP]
by (intro prems(2) gx1) simp_all
[PROOF STATE]
proof (state)
this:
0 < f2' ((ts ! i) x)

goal (2 subgoals):
 1. finite {..<k}
 2. \<And>x. x \<in> {..<k} \<Longrightarrow> 0 \<le> as ! x * f2' ((ts ! x) x)
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
i \<in> {..<k}
0 < f2' ((ts ! i) x)
[PROOF STEP]
show "as!i * f2' ((ts!i) x) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
i \<in> {..<k}
0 < f2' ((ts ! i) x)

goal (1 subgoal):
 1. 0 \<le> as ! i * f2' ((ts ! i) x)
[PROOF STEP]
by (intro mult_nonneg_nonneg[OF a_ge_0]) simp_all
[PROOF STATE]
proof (state)
this:
0 \<le> as ! i * f2' ((ts ! i) x)

goal (1 subgoal):
 1. finite {..<k}
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
0 < (\<Sum>i<k. as ! i * f2' ((ts ! i) x))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>gx1 \<le> x; \<And>xa. \<lbrakk>xa \<in> {..<k}; gx0 \<le> (ts ! xa) x\<rbrakk> \<Longrightarrow> 0 < f2' ((ts ! xa) x); gx0 \<le> x\<rbrakk> \<Longrightarrow> 0 < f2' x
[PROOF STEP]
with prems(1) gx0_le_gx1
[PROOF STATE]
proof (chain)
picking this:
gx1 \<le> x
gx0 \<le> gx1
0 < (\<Sum>i<k. as ! i * f2' ((ts ! i) x))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
gx1 \<le> x
gx0 \<le> gx1
0 < (\<Sum>i<k. as ! i * f2' ((ts ! i) x))

goal (1 subgoal):
 1. 0 < f2' x
[PROOF STEP]
by (auto intro!: add_nonneg_pos gx0)
[PROOF STATE]
proof (state)
this:
0 < f2' x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < f2' x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma listToFun_futz:
  "\<lbrakk> M \<in> set (listToFun xs); x \<in> fst ` set xs \<rbrakk>
     \<Longrightarrow> M x \<in> { y |y ys. (x, ys) \<in> set xs \<and> y \<in> set ys}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>M \<in> set (listToFun xs); x \<in> fst ` set xs\<rbrakk> \<Longrightarrow> M x \<in> {uu_. \<exists>y ys. uu_ = y \<and> (x, ys) \<in> set xs \<and> y \<in> set ys}
[PROOF STEP]
unfolding listToFun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>M \<in> set (foldr (\<lambda>(a, acts) M. concat (map (\<lambda>m. map (fun_upd m a) acts) M)) xs [\<lambda>_. undefined]); x \<in> fst ` set xs\<rbrakk> \<Longrightarrow> M x \<in> {uu_. \<exists>y ys. uu_ = y \<and> (x, ys) \<in> set xs \<and> y \<in> set ys}
[PROOF STEP]
apply (induct xs arbitrary: M)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M. \<lbrakk>M \<in> set (foldr (\<lambda>(a, acts) M. concat (map (\<lambda>m. map (fun_upd m a) acts) M)) [] [\<lambda>_. undefined]); x \<in> fst ` set []\<rbrakk> \<Longrightarrow> M x \<in> {uu_. \<exists>y ys. uu_ = y \<and> (x, ys) \<in> set [] \<and> y \<in> set ys}
 2. \<And>a xs M. \<lbrakk>\<And>M. \<lbrakk>M \<in> set (foldr (\<lambda>(a, acts) M. concat (map (\<lambda>m. map (fun_upd m a) acts) M)) xs [\<lambda>_. undefined]); x \<in> fst ` set xs\<rbrakk> \<Longrightarrow> M x \<in> {uu_. \<exists>y ys. uu_ = y \<and> (x, ys) \<in> set xs \<and> y \<in> set ys}; M \<in> set (foldr (\<lambda>(a, acts) M. concat (map (\<lambda>m. map (fun_upd m a) acts) M)) (a # xs) [\<lambda>_. undefined]); x \<in> fst ` set (a # xs)\<rbrakk> \<Longrightarrow> M x \<in> {uu_. \<exists>y ys. uu_ = y \<and> (x, ys) \<in> set (a # xs) \<and> y \<in> set ys}
[PROOF STEP]
apply (simp_all add: split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs M. \<lbrakk>\<And>M. \<lbrakk>M \<in> set (foldr (\<lambda>p M. concat (map (\<lambda>m. map (fun_upd m (fst p)) (snd p)) M)) xs [\<lambda>_. undefined]); x \<in> fst ` set xs\<rbrakk> \<Longrightarrow> \<exists>ys. (x, ys) \<in> set xs \<and> M x \<in> set ys; \<exists>x\<in>set (foldr (\<lambda>p M. concat (map (\<lambda>m. map (fun_upd m (fst p)) (snd p)) M)) xs [\<lambda>_. undefined]). M \<in> fun_upd x (fst a) ` set (snd a); x = fst a \<or> x \<in> fst ` set xs\<rbrakk> \<Longrightarrow> \<exists>ys. ((x, ys) = a \<or> (x, ys) \<in> set xs) \<and> M x \<in> set ys
[PROOF STEP]
apply (case_tac a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs M aa b. \<lbrakk>\<And>M. \<lbrakk>M \<in> set (foldr (\<lambda>p M. concat (map (\<lambda>m. map (fun_upd m (fst p)) (snd p)) M)) xs [\<lambda>_. undefined]); x \<in> fst ` set xs\<rbrakk> \<Longrightarrow> \<exists>ys. (x, ys) \<in> set xs \<and> M x \<in> set ys; \<exists>x\<in>set (foldr (\<lambda>p M. concat (map (\<lambda>m. map (fun_upd m (fst p)) (snd p)) M)) xs [\<lambda>_. undefined]). M \<in> fun_upd x (fst a) ` set (snd a); x = fst a \<or> x \<in> fst ` set xs; a = (aa, b)\<rbrakk> \<Longrightarrow> \<exists>ys. ((x, ys) = a \<or> (x, ys) \<in> set xs) \<and> M x \<in> set ys
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs aa ba xa xaa. \<lbrakk>\<And>M. \<lbrakk>M \<in> set (foldr (\<lambda>p M. concat (map (\<lambda>m. map (fun_upd m (fst p)) (snd p)) M)) xs [\<lambda>_. undefined]); x \<in> fst ` set xs\<rbrakk> \<Longrightarrow> \<exists>ys. (x, ys) \<in> set xs \<and> M x \<in> set ys; x = aa \<or> x \<in> fst ` set xs; xa \<in> set (foldr (\<lambda>p M. concat (map (\<lambda>m. map (fun_upd m (fst p)) (snd p)) M)) xs [\<lambda>_. undefined]); xaa \<in> set ba\<rbrakk> \<Longrightarrow> (x = aa \<longrightarrow> (\<exists>ys. (ys = ba \<or> (aa, ys) \<in> set xs) \<and> xaa \<in> set ys)) \<and> (x \<noteq> aa \<longrightarrow> (\<exists>ys. (x, ys) \<in> set xs \<and> xa x \<in> set ys))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma finite_sum_nth_digit_commute2:
  fixes M :: nat
  shows "\<forall>t. \<forall>k\<le>M. nth_digit (fct k) t b < 2^c \<Longrightarrow>
         \<forall>t. \<forall>m\<le>M. nth_digit (\<Sum>i=0..m. fct i) t b < 2^c \<Longrightarrow>
         nth_digit (\<Sum>i=0..M. fct i) t b = (\<Sum>i=0..M. (nth_digit (fct i) t b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b)
[PROOF STEP]
proof (induct M arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>\<forall>t k. k \<le> 0 \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> 0 \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..0}) t b = (\<Sum>i = 0..0. nth_digit (fct i) t b)
 2. \<And>M t. \<lbrakk>\<And>t. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b); \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<forall>t k. k \<le> 0 \<longrightarrow> nth_digit (fct k) t b < 2 ^ c
\<forall>t m. m \<le> 0 \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c

goal (2 subgoals):
 1. \<And>t. \<lbrakk>\<forall>t k. k \<le> 0 \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> 0 \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..0}) t b = (\<Sum>i = 0..0. nth_digit (fct i) t b)
 2. \<And>M t. \<lbrakk>\<And>t. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b); \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>t k. k \<le> 0 \<longrightarrow> nth_digit (fct k) t b < 2 ^ c
\<forall>t m. m \<le> 0 \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c

goal (1 subgoal):
 1. nth_digit (sum fct {0..0}) t b = (\<Sum>i = 0..0. nth_digit (fct i) t b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nth_digit (sum fct {0..0}) t b = (\<Sum>i = 0..0. nth_digit (fct i) t b)

goal (1 subgoal):
 1. \<And>M t. \<lbrakk>\<And>t. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b); \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M t. \<lbrakk>\<And>t. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b); \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
case (Suc M)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) ?t b = (\<Sum>i = 0..M. nth_digit (fct i) ?t b)
\<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c
\<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c

goal (1 subgoal):
 1. \<And>M t. \<lbrakk>\<And>t. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b); \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
have assm1: "\<forall>t. \<forall>k\<le>Suc M. nth_digit (fct k) t b < 2^c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
\<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c
\<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c

goal (1 subgoal):
 1. \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c

goal (1 subgoal):
 1. \<And>M t. \<lbrakk>\<And>t. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b); \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
have assm1_reduced: "\<forall>t. \<forall>k\<le>M. nth_digit (fct k) t b < 2^c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c
[PROOF STEP]
using assm1
[PROOF STATE]
proof (prove)
using this:
\<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c

goal (1 subgoal):
 1. \<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c

goal (1 subgoal):
 1. \<And>M t. \<lbrakk>\<And>t. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b); \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
have nocarry2: "\<forall>t. \<forall>k\<le>Suc M. nth_digit (fct k) t b \<exclamdown> c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b \<exclamdown> c = 0
[PROOF STEP]
using assm1 nth_bit_def
[PROOF STATE]
proof (prove)
using this:
\<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c
?num \<exclamdown> ?k = ?num div 2 ^ ?k mod 2

goal (1 subgoal):
 1. \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b \<exclamdown> c = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b \<exclamdown> c = 0

goal (1 subgoal):
 1. \<And>M t. \<lbrakk>\<And>t. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b); \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
have assm2:
    "\<forall>t. nth_digit (\<Sum>i=0..M. (fct i)) t b < 2^c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. nth_digit (sum fct {0..M}) t b < 2 ^ c
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
\<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c
\<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c

goal (1 subgoal):
 1. \<forall>t. nth_digit (sum fct {0..M}) t b < 2 ^ c
[PROOF STEP]
by (simp add: add.commute)
[PROOF STATE]
proof (state)
this:
\<forall>t. nth_digit (sum fct {0..M}) t b < 2 ^ c

goal (1 subgoal):
 1. \<And>M t. \<lbrakk>\<And>t. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b); \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
hence nocarry3: "\<forall>t. nth_digit (\<Sum>i=0..M. fct i) t b \<exclamdown> c = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>t. nth_digit (sum fct {0..M}) t b < 2 ^ c

goal (1 subgoal):
 1. \<forall>t. nth_digit (sum fct {0..M}) t b \<exclamdown> c = 0
[PROOF STEP]
using aux_lt_implies_mask
[PROOF STATE]
proof (prove)
using this:
\<forall>t. nth_digit (sum fct {0..M}) t b < 2 ^ c
?a < 2 ^ ?k \<Longrightarrow> \<forall>r\<ge>?k. ?a \<exclamdown> r = 0

goal (1 subgoal):
 1. \<forall>t. nth_digit (sum fct {0..M}) t b \<exclamdown> c = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>t. nth_digit (sum fct {0..M}) t b \<exclamdown> c = 0

goal (1 subgoal):
 1. \<And>M t. \<lbrakk>\<And>t. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b); \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
have 1: "nth_digit (sum fct {0..M}) (t - 1) b \<exclamdown> c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_digit (sum fct {0..M}) (t - 1) b \<exclamdown> c = 0
[PROOF STEP]
using nocarry3
[PROOF STATE]
proof (prove)
using this:
\<forall>t. nth_digit (sum fct {0..M}) t b \<exclamdown> c = 0

goal (1 subgoal):
 1. nth_digit (sum fct {0..M}) (t - 1) b \<exclamdown> c = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nth_digit (sum fct {0..M}) (t - 1) b \<exclamdown> c = 0

goal (1 subgoal):
 1. \<And>M t. \<lbrakk>\<And>t. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b); \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
have 2: "nth_digit (fct (Suc M)) (t - 1) b \<exclamdown> c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_digit (fct (Suc M)) (t - 1) b \<exclamdown> c = 0
[PROOF STEP]
using nocarry2
[PROOF STATE]
proof (prove)
using this:
\<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b \<exclamdown> c = 0

goal (1 subgoal):
 1. nth_digit (fct (Suc M)) (t - 1) b \<exclamdown> c = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nth_digit (fct (Suc M)) (t - 1) b \<exclamdown> c = 0

goal (1 subgoal):
 1. \<And>M t. \<lbrakk>\<And>t. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b); \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
have 3: "nth_digit (sum fct {0..M}) t b \<exclamdown> c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_digit (sum fct {0..M}) t b \<exclamdown> c = 0
[PROOF STEP]
using nocarry3
[PROOF STATE]
proof (prove)
using this:
\<forall>t. nth_digit (sum fct {0..M}) t b \<exclamdown> c = 0

goal (1 subgoal):
 1. nth_digit (sum fct {0..M}) t b \<exclamdown> c = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nth_digit (sum fct {0..M}) t b \<exclamdown> c = 0

goal (1 subgoal):
 1. \<And>M t. \<lbrakk>\<And>t. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b); \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
have 4: "nth_digit (fct (Suc M)) t b \<exclamdown> c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_digit (fct (Suc M)) t b \<exclamdown> c = 0
[PROOF STEP]
using nocarry2
[PROOF STATE]
proof (prove)
using this:
\<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b \<exclamdown> c = 0

goal (1 subgoal):
 1. nth_digit (fct (Suc M)) t b \<exclamdown> c = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nth_digit (fct (Suc M)) t b \<exclamdown> c = 0

goal (1 subgoal):
 1. \<And>M t. \<lbrakk>\<And>t. \<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) t b = (\<Sum>i = 0..M. nth_digit (fct i) t b); \<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
from block_additivity
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 < ?c; nth_digit ?x (?t - 1) (2 ^ Suc ?c) \<exclamdown> ?c = 0; nth_digit ?y (?t - 1) (2 ^ Suc ?c) \<exclamdown> ?c = 0; nth_digit ?x ?t (2 ^ Suc ?c) \<exclamdown> ?c = 0; nth_digit ?y ?t (2 ^ Suc ?c) \<exclamdown> ?c = 0\<rbrakk> \<Longrightarrow> nth_digit (?x + ?y) ?t (2 ^ Suc ?c) = nth_digit ?x ?t (2 ^ Suc ?c) + nth_digit ?y ?t (2 ^ Suc ?c)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ?c; nth_digit ?x (?t - 1) (2 ^ Suc ?c) \<exclamdown> ?c = 0; nth_digit ?y (?t - 1) (2 ^ Suc ?c) \<exclamdown> ?c = 0; nth_digit ?x ?t (2 ^ Suc ?c) \<exclamdown> ?c = 0; nth_digit ?y ?t (2 ^ Suc ?c) \<exclamdown> ?c = 0\<rbrakk> \<Longrightarrow> nth_digit (?x + ?y) ?t (2 ^ Suc ?c) = nth_digit ?x ?t (2 ^ Suc ?c) + nth_digit ?y ?t (2 ^ Suc ?c)

goal (1 subgoal):
 1. nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
using 1 2 3 4 c_gt0 Suc b_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ?c; nth_digit ?x (?t - 1) (2 ^ Suc ?c) \<exclamdown> ?c = 0; nth_digit ?y (?t - 1) (2 ^ Suc ?c) \<exclamdown> ?c = 0; nth_digit ?x ?t (2 ^ Suc ?c) \<exclamdown> ?c = 0; nth_digit ?y ?t (2 ^ Suc ?c) \<exclamdown> ?c = 0\<rbrakk> \<Longrightarrow> nth_digit (?x + ?y) ?t (2 ^ Suc ?c) = nth_digit ?x ?t (2 ^ Suc ?c) + nth_digit ?y ?t (2 ^ Suc ?c)
nth_digit (sum fct {0..M}) (t - 1) b \<exclamdown> c = 0
nth_digit (fct (Suc M)) (t - 1) b \<exclamdown> c = 0
nth_digit (sum fct {0..M}) t b \<exclamdown> c = 0
nth_digit (fct (Suc M)) t b \<exclamdown> c = 0
0 < c
\<lbrakk>\<forall>t k. k \<le> M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c; \<forall>t m. m \<le> M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c\<rbrakk> \<Longrightarrow> nth_digit (sum fct {0..M}) ?t b = (\<Sum>i = 0..M. nth_digit (fct i) ?t b)
\<forall>t k. k \<le> Suc M \<longrightarrow> nth_digit (fct k) t b < 2 ^ c
\<forall>t m. m \<le> Suc M \<longrightarrow> nth_digit (sum fct {0..m}) t b < 2 ^ c
b \<equiv> 2 ^ Suc c

goal (1 subgoal):
 1. nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nth_digit (sum fct {0..Suc M}) t b = (\<Sum>i = 0..Suc M. nth_digit (fct i) t b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval_Mn_convergI:
  assumes "recfn (length xs) (Mn n f)"
    and "eval f (z # xs) \<down>= 0"
    and "\<And>y. y < z \<Longrightarrow> eval f (y # xs) \<down>\<noteq> 0"
  shows "eval (Mn n f) xs \<down>= z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Mn n f) xs \<down>= z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval (Mn n f) xs \<down>= z
[PROOF STEP]
let ?P = "\<lambda>z. eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval (Mn n f) xs \<down>= z
[PROOF STEP]
have "z = Least ?P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z = (LEAST z. eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>))
[PROOF STEP]
using Least_equality[of ?P z] assms(2,3) not_le_imp_less
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>); \<And>y. eval f (y # xs) \<down>= 0 \<and> (\<forall>ya<y. eval f (ya # xs) \<down>) \<Longrightarrow> z \<le> y\<rbrakk> \<Longrightarrow> (LEAST z. eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>)) = z
eval f (z # xs) \<down>= 0
?y < z \<Longrightarrow> eval f (?y # xs) \<down>\<noteq> 0
\<not> ?y \<le> ?x \<Longrightarrow> ?x < ?y

goal (1 subgoal):
 1. z = (LEAST z. eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z = (LEAST z. eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>))

goal (1 subgoal):
 1. eval (Mn n f) xs \<down>= z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
z = (LEAST z. eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>))

goal (1 subgoal):
 1. eval (Mn n f) xs \<down>= z
[PROOF STEP]
have "?P z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>)
[PROOF STEP]
using assms(2,3)
[PROOF STATE]
proof (prove)
using this:
eval f (z # xs) \<down>= 0
?y < z \<Longrightarrow> eval f (?y # xs) \<down>\<noteq> 0

goal (1 subgoal):
 1. eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>)

goal (1 subgoal):
 1. eval (Mn n f) xs \<down>= z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
z = (LEAST z. eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>))
eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>)
[PROOF STEP]
show "eval (Mn n f) xs \<down>= z"
[PROOF STATE]
proof (prove)
using this:
z = (LEAST z. eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>))
eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>)

goal (1 subgoal):
 1. eval (Mn n f) xs \<down>= z
[PROOF STEP]
using eval_Mn[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
z = (LEAST z. eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>))
eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>)
eval (Mn n f) xs = (if \<exists>z. eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>) then Some (LEAST z. eval f (z # xs) \<down>= 0 \<and> (\<forall>y<z. eval f (y # xs) \<down>)) else None)

goal (1 subgoal):
 1. eval (Mn n f) xs \<down>= z
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
eval (Mn n f) xs \<down>= z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tuple_decode_encode' [simp]:
  assumes "length xs = Suc n"
  shows "tuple_decode n (tuple_encode n xs) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tuple_decode n (tuple_encode n xs) = xs
[PROOF STEP]
using assms tuple_decode_encode
[PROOF STATE]
proof (prove)
using this:
length xs = Suc n
0 < length ?xs \<Longrightarrow> tuple_decode (length ?xs - 1) (tuple_encode (length ?xs - 1) ?xs) = ?xs

goal (1 subgoal):
 1. tuple_decode n (tuple_encode n xs) = xs
[PROOF STEP]
by (metis diff_Suc_1 zero_less_Suc)