[STATEMENT]
lemma sub2_wit_norms_mus':
  assumes "n_gs' = map (\<lambda>v. (v, sq_norm_vec v)) gs'"
   "sub2_wit gs' fs = (mus, gs)" "set fs \<subseteq> carrier_vec n" "set gs' \<subseteq> carrier_vec n"
 shows "norms_mus' fs n_gs' mus_acc = (map sq_norm_vec (rev gs @ gs'), rev mus @ mus_acc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norms_mus' fs n_gs' mus_acc = (map sq_norm (rev gs @ gs'), rev mus @ mus_acc)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n_gs' = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'
sub2_wit gs' fs = (mus, gs)
set fs \<subseteq> carrier_vec n
set gs' \<subseteq> carrier_vec n

goal (1 subgoal):
 1. norms_mus' fs n_gs' mus_acc = (map sq_norm (rev gs @ gs'), rev mus @ mus_acc)
[PROOF STEP]
proof (induction fs n_gs' mus_acc arbitrary: gs' mus gs rule: norms_mus'.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n_gs mus gs' musa gs. \<lbrakk>n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' [] = (musa, gs); set [] \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' [] n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
 2. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
case (1 n_gs mus_acc)
[PROOF STATE]
proof (state)
this:
n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'
sub2_wit gs' [] = (mus, gs)
set [] \<subseteq> carrier_vec n
set gs' \<subseteq> carrier_vec n

goal (2 subgoals):
 1. \<And>n_gs mus gs' musa gs. \<lbrakk>n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' [] = (musa, gs); set [] \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' [] n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
 2. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'
sub2_wit gs' [] = (mus, gs)
set [] \<subseteq> carrier_vec n
set gs' \<subseteq> carrier_vec n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'
sub2_wit gs' [] = (mus, gs)
set [] \<subseteq> carrier_vec n
set gs' \<subseteq> carrier_vec n

goal (1 subgoal):
 1. norms_mus' [] n_gs mus_acc = (map sq_norm (rev gs @ gs'), rev mus @ mus_acc)
[PROOF STEP]
by (auto simp add: rev_map)
[PROOF STATE]
proof (state)
this:
norms_mus' [] n_gs mus_acc = (map sq_norm (rev gs @ gs'), rev mus @ mus_acc)

goal (1 subgoal):
 1. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
case (2  f fs n_gs mus_acc)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x3 = mus_adjuster f n_gs [] (0\<^sub>v n); (?xa3, ?y3) = ?x3; ?xb3 = ?y3 + f; (?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) ?gs'3; sub2_wit ?gs'3 fs = (?mus3, ?gs3); set fs \<subseteq> carrier_vec n; set ?gs'3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs) (?xa3 # mus_acc) = (map sq_norm (rev ?gs3 @ ?gs'3), rev ?mus3 @ ?xa3 # mus_acc)
n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'
sub2_wit gs' (f # fs) = (mus, gs)
set (f # fs) \<subseteq> carrier_vec n
set gs' \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
note aw1 = conjunct1[OF conjunct2[OF gram_schmidt_fs.adjuster_wit]]
[PROOF STATE]
proof (state)
this:
\<lbrakk>gram_schmidt.adjuster_wit ?n2 ?wits2 ?w2 ?us2 = (?wits'2, ?a2); ?w2 \<in> carrier_vec ?n2; \<And>i. i \<le> ?j2 \<Longrightarrow> ?fs2 ! i \<in> carrier_vec ?n2; ?us2 = map (gram_schmidt_fs.gso ?n2 ?fs2) (rev [0..<?j2]); ?wits2 = map (gram_schmidt_fs.\<mu> ?n2 ?fs2 ?i2) [?j2..<?i2]; ?j2 \<le> ?n2; ?j2 \<le> ?i2; ?w2 = ?fs2 ! ?i2\<rbrakk> \<Longrightarrow> ?a2 \<in> carrier_vec ?n2

goal (1 subgoal):
 1. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
let ?aw = "mus_adjuster f n_gs [] (0\<^sub>v n)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
have aw: "?aw = adjuster_wit [] f gs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mus_adjuster f n_gs [] (0\<^sub>v n) = adjuster_wit [] f gs'
[PROOF STEP]
apply(subst adjuster_wit')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) ?gs
 2. f \<in> carrier_vec n
 3. set ?gs \<subseteq> carrier_vec n
 4. adjuster_wit [] f ?gs = adjuster_wit [] f gs'
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3 = mus_adjuster f n_gs [] (0\<^sub>v n); (?xa3, ?y3) = ?x3; ?xb3 = ?y3 + f; (?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) ?gs'3; sub2_wit ?gs'3 fs = (?mus3, ?gs3); set fs \<subseteq> carrier_vec n; set ?gs'3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs) (?xa3 # mus_acc) = (map sq_norm (rev ?gs3 @ ?gs'3), rev ?mus3 @ ?xa3 # mus_acc)
n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'
sub2_wit gs' (f # fs) = (mus, gs)
set (f # fs) \<subseteq> carrier_vec n
set gs' \<subseteq> carrier_vec n

goal (4 subgoals):
 1. n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) ?gs
 2. f \<in> carrier_vec n
 3. set ?gs \<subseteq> carrier_vec n
 4. adjuster_wit [] f ?gs = adjuster_wit [] f gs'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mus_adjuster f n_gs [] (0\<^sub>v n) = adjuster_wit [] f gs'

goal (1 subgoal):
 1. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
have "sub2_wit ((snd ?aw + f) # gs') fs = sub2_wit ((snd (adjuster_wit [] f gs') + f) # gs') fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub2_wit ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') fs = sub2_wit ((snd (adjuster_wit [] f gs') + f) # gs') fs
[PROOF STEP]
apply(subst adjuster_wit')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) ?gs
 2. f \<in> carrier_vec n
 3. set ?gs \<subseteq> carrier_vec n
 4. sub2_wit ((snd (adjuster_wit [] f ?gs) + f) # gs') fs = sub2_wit ((snd (adjuster_wit [] f gs') + f) # gs') fs
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3 = mus_adjuster f n_gs [] (0\<^sub>v n); (?xa3, ?y3) = ?x3; ?xb3 = ?y3 + f; (?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) ?gs'3; sub2_wit ?gs'3 fs = (?mus3, ?gs3); set fs \<subseteq> carrier_vec n; set ?gs'3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs) (?xa3 # mus_acc) = (map sq_norm (rev ?gs3 @ ?gs'3), rev ?mus3 @ ?xa3 # mus_acc)
n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'
sub2_wit gs' (f # fs) = (mus, gs)
set (f # fs) \<subseteq> carrier_vec n
set gs' \<subseteq> carrier_vec n

goal (4 subgoals):
 1. n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) ?gs
 2. f \<in> carrier_vec n
 3. set ?gs \<subseteq> carrier_vec n
 4. sub2_wit ((snd (adjuster_wit [] f ?gs) + f) # gs') fs = sub2_wit ((snd (adjuster_wit [] f gs') + f) # gs') fs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sub2_wit ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') fs = sub2_wit ((snd (adjuster_wit [] f gs') + f) # gs') fs

goal (1 subgoal):
 1. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sub2_wit ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') fs = sub2_wit ((snd (adjuster_wit [] f gs') + f) # gs') fs

goal (1 subgoal):
 1. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
have "\<dots> = (tl mus, tl gs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub2_wit ((snd (adjuster_wit [] f gs') + f) # gs') fs = (tl mus, tl gs)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3 = mus_adjuster f n_gs [] (0\<^sub>v n); (?xa3, ?y3) = ?x3; ?xb3 = ?y3 + f; (?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) ?gs'3; sub2_wit ?gs'3 fs = (?mus3, ?gs3); set fs \<subseteq> carrier_vec n; set ?gs'3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs) (?xa3 # mus_acc) = (map sq_norm (rev ?gs3 @ ?gs'3), rev ?mus3 @ ?xa3 # mus_acc)
n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'
sub2_wit gs' (f # fs) = (mus, gs)
set (f # fs) \<subseteq> carrier_vec n
set gs' \<subseteq> carrier_vec n

goal (1 subgoal):
 1. sub2_wit ((snd (adjuster_wit [] f gs') + f) # gs') fs = (tl mus, tl gs)
[PROOF STEP]
by (auto simp add: Let_def case_prod_beta')
[PROOF STATE]
proof (state)
this:
sub2_wit ((snd (adjuster_wit [] f gs') + f) # gs') fs = (tl mus, tl gs)

goal (1 subgoal):
 1. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sub2_wit ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') fs = (tl mus, tl gs)
[PROOF STEP]
have sub_tl: "sub2_wit ((snd ?aw + f) # gs') fs = (tl mus, tl gs)"
[PROOF STATE]
proof (prove)
using this:
sub2_wit ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') fs = (tl mus, tl gs)

goal (1 subgoal):
 1. sub2_wit ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') fs = (tl mus, tl gs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sub2_wit ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') fs = (tl mus, tl gs)

goal (1 subgoal):
 1. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
have aw_c: "snd ?aw \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (mus_adjuster f n_gs [] (0\<^sub>v n)) \<in> carrier_vec n
[PROOF STEP]
apply(subst adjuster_wit'[of _ gs'])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs'
 2. f \<in> carrier_vec n
 3. set gs' \<subseteq> carrier_vec n
 4. snd (adjuster_wit [] f gs') \<in> carrier_vec n
[PROOF STEP]
using 2 adjuster_wit_carrier_vec
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3 = mus_adjuster f n_gs [] (0\<^sub>v n); (?xa3, ?y3) = ?x3; ?xb3 = ?y3 + f; (?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) ?gs'3; sub2_wit ?gs'3 fs = (?mus3, ?gs3); set fs \<subseteq> carrier_vec n; set ?gs'3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs) (?xa3 # mus_acc) = (map sq_norm (rev ?gs3 @ ?gs'3), rev ?mus3 @ ?xa3 # mus_acc)
n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'
sub2_wit gs' (f # fs) = (mus, gs)
set (f # fs) \<subseteq> carrier_vec n
set gs' \<subseteq> carrier_vec n
\<lbrakk>?f \<in> carrier_vec n; set ?gs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> snd (adjuster_wit ?mus ?f ?gs) \<in> carrier_vec n

goal (4 subgoals):
 1. n_gs = map (\<lambda>x. (x, \<parallel>x\<parallel>\<^sup>2)) gs'
 2. f \<in> carrier_vec n
 3. set gs' \<subseteq> carrier_vec n
 4. snd (adjuster_wit [] f gs') \<in> carrier_vec n
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
snd (mus_adjuster f n_gs [] (0\<^sub>v n)) \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
have gs: "gs = (snd ?aw + f) # tl gs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs = (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # tl gs
[PROOF STEP]
apply(subst aw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs = (snd (adjuster_wit [] f gs') + f) # tl gs
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3 = mus_adjuster f n_gs [] (0\<^sub>v n); (?xa3, ?y3) = ?x3; ?xb3 = ?y3 + f; (?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) ?gs'3; sub2_wit ?gs'3 fs = (?mus3, ?gs3); set fs \<subseteq> carrier_vec n; set ?gs'3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs) (?xa3 # mus_acc) = (map sq_norm (rev ?gs3 @ ?gs'3), rev ?mus3 @ ?xa3 # mus_acc)
n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'
sub2_wit gs' (f # fs) = (mus, gs)
set (f # fs) \<subseteq> carrier_vec n
set gs' \<subseteq> carrier_vec n

goal (1 subgoal):
 1. gs = (snd (adjuster_wit [] f gs') + f) # tl gs
[PROOF STEP]
by (auto simp add: Let_def case_prod_beta')
[PROOF STATE]
proof (state)
this:
gs = (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # tl gs

goal (1 subgoal):
 1. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
have mus: "mus = fst ?aw # tl mus"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mus = fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # tl mus
[PROOF STEP]
apply(subst aw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mus = fst (adjuster_wit [] f gs') # tl mus
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3 = mus_adjuster f n_gs [] (0\<^sub>v n); (?xa3, ?y3) = ?x3; ?xb3 = ?y3 + f; (?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) ?gs'3; sub2_wit ?gs'3 fs = (?mus3, ?gs3); set fs \<subseteq> carrier_vec n; set ?gs'3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs) (?xa3 # mus_acc) = (map sq_norm (rev ?gs3 @ ?gs'3), rev ?mus3 @ ?xa3 # mus_acc)
n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'
sub2_wit gs' (f # fs) = (mus, gs)
set (f # fs) \<subseteq> carrier_vec n
set gs' \<subseteq> carrier_vec n

goal (1 subgoal):
 1. mus = fst (adjuster_wit [] f gs') # tl mus
[PROOF STEP]
by (auto simp add: Let_def case_prod_beta')
[PROOF STATE]
proof (state)
this:
mus = fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # tl mus

goal (1 subgoal):
 1. \<And>f fs n_gs mus gs' musa gs. \<lbrakk>\<And>x xa y xb gs' musa gs. \<lbrakk>x = mus_adjuster f n_gs [] (0\<^sub>v n); (xa, y) = x; xb = y + f; (xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' fs = (musa, gs); set fs \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((xb, \<parallel>xb\<parallel>\<^sup>2) # n_gs) (xa # mus) = (map sq_norm (rev gs @ gs'), rev musa @ xa # mus); n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'; sub2_wit gs' (f # fs) = (musa, gs); set (f # fs) \<subseteq> carrier_vec n; set gs' \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' (f # fs) n_gs mus = (map sq_norm (rev gs @ gs'), rev musa @ mus)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norms_mus' (f # fs) n_gs mus_acc = (map sq_norm (rev gs @ gs'), rev mus @ mus_acc)
[PROOF STEP]
apply(simp add: Let_def case_prod_beta')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norms_mus' fs ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f, \<parallel>snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f\<parallel>\<^sup>2) # n_gs) (fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # mus_acc) = (map sq_norm (rev gs) @ map sq_norm gs', rev mus @ mus_acc)
[PROOF STEP]
apply(subst 2(1)[of _ _ _ _ "(snd ?aw + f)#gs'"  "tl mus" "tl gs"])
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. ?x = mus_adjuster f n_gs [] (0\<^sub>v n)
 2. (fst (mus_adjuster f n_gs [] (0\<^sub>v n)), ?y) = ?x
 3. snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f = ?y + f
 4. (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f, \<parallel>snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs')
 5. sub2_wit ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') fs = (tl mus, tl gs)
 6. set fs \<subseteq> carrier_vec n
 7. set ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') \<subseteq> carrier_vec n
 8. (map sq_norm (rev (tl gs) @ (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs'), rev (tl mus) @ fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # mus_acc) = (map sq_norm (rev gs) @ map sq_norm gs', rev mus @ mus_acc)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. (fst (mus_adjuster f n_gs [] (0\<^sub>v n)), ?y) = mus_adjuster f n_gs [] (0\<^sub>v n)
 2. snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f = ?y + f
 3. (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f, \<parallel>snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs')
 4. sub2_wit ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') fs = (tl mus, tl gs)
 5. set fs \<subseteq> carrier_vec n
 6. set ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') \<subseteq> carrier_vec n
 7. (map sq_norm (rev (tl gs) @ (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs'), rev (tl mus) @ fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # mus_acc) = (map sq_norm (rev gs) @ map sq_norm gs', rev mus @ mus_acc)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f = ?y + f
 2. (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f, \<parallel>snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs')
 3. sub2_wit ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') fs = (tl mus, tl gs)
 4. set fs \<subseteq> carrier_vec n
 5. set ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') \<subseteq> carrier_vec n
 6. (map sq_norm (rev (tl gs) @ (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs'), rev (tl mus) @ fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # mus_acc) = (map sq_norm (rev gs) @ map sq_norm gs', rev mus @ mus_acc)
 7. (fst (mus_adjuster f n_gs [] (0\<^sub>v n)), ?y) = mus_adjuster f n_gs [] (0\<^sub>v n)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f, \<parallel>snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs')
 2. sub2_wit ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') fs = (tl mus, tl gs)
 3. set fs \<subseteq> carrier_vec n
 4. set ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') \<subseteq> carrier_vec n
 5. (map sq_norm (rev (tl gs) @ (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs'), rev (tl mus) @ fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # mus_acc) = (map sq_norm (rev gs) @ map sq_norm gs', rev mus @ mus_acc)
 6. (fst (mus_adjuster f n_gs [] (0\<^sub>v n)), snd (mus_adjuster f n_gs [] (0\<^sub>v n))) = mus_adjuster f n_gs [] (0\<^sub>v n)
[PROOF STEP]
apply (simp add: "2.prems"(1))
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. sub2_wit ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') fs = (tl mus, tl gs)
 2. set fs \<subseteq> carrier_vec n
 3. set ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') \<subseteq> carrier_vec n
 4. (map sq_norm (rev (tl gs) @ (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs'), rev (tl mus) @ fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # mus_acc) = (map sq_norm (rev gs) @ map sq_norm gs', rev mus @ mus_acc)
 5. (fst (mus_adjuster f n_gs [] (0\<^sub>v n)), snd (mus_adjuster f n_gs [] (0\<^sub>v n))) = mus_adjuster f n_gs [] (0\<^sub>v n)
[PROOF STEP]
using sub_tl
[PROOF STATE]
proof (prove)
using this:
sub2_wit ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') fs = (tl mus, tl gs)

goal (5 subgoals):
 1. sub2_wit ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') fs = (tl mus, tl gs)
 2. set fs \<subseteq> carrier_vec n
 3. set ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') \<subseteq> carrier_vec n
 4. (map sq_norm (rev (tl gs) @ (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs'), rev (tl mus) @ fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # mus_acc) = (map sq_norm (rev gs) @ map sq_norm gs', rev mus @ mus_acc)
 5. (fst (mus_adjuster f n_gs [] (0\<^sub>v n)), snd (mus_adjuster f n_gs [] (0\<^sub>v n))) = mus_adjuster f n_gs [] (0\<^sub>v n)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. set fs \<subseteq> carrier_vec n
 2. set ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') \<subseteq> carrier_vec n
 3. (map sq_norm (rev (tl gs) @ (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs'), rev (tl mus) @ fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # mus_acc) = (map sq_norm (rev gs) @ map sq_norm gs', rev mus @ mus_acc)
 4. (fst (mus_adjuster f n_gs [] (0\<^sub>v n)), snd (mus_adjuster f n_gs [] (0\<^sub>v n))) = mus_adjuster f n_gs [] (0\<^sub>v n)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3 = mus_adjuster f n_gs [] (0\<^sub>v n); (?xa3, ?y3) = ?x3; ?xb3 = ?y3 + f; (?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) ?gs'3; sub2_wit ?gs'3 fs = (?mus3, ?gs3); set fs \<subseteq> carrier_vec n; set ?gs'3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs) (?xa3 # mus_acc) = (map sq_norm (rev ?gs3 @ ?gs'3), rev ?mus3 @ ?xa3 # mus_acc)
n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'
sub2_wit gs' (f # fs) = (mus, gs)
set (f # fs) \<subseteq> carrier_vec n
set gs' \<subseteq> carrier_vec n

goal (4 subgoals):
 1. set fs \<subseteq> carrier_vec n
 2. set ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') \<subseteq> carrier_vec n
 3. (map sq_norm (rev (tl gs) @ (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs'), rev (tl mus) @ fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # mus_acc) = (map sq_norm (rev gs) @ map sq_norm gs', rev mus @ mus_acc)
 4. (fst (mus_adjuster f n_gs [] (0\<^sub>v n)), snd (mus_adjuster f n_gs [] (0\<^sub>v n))) = mus_adjuster f n_gs [] (0\<^sub>v n)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. set ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') \<subseteq> carrier_vec n
 2. (map sq_norm (rev (tl gs) @ (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs'), rev (tl mus) @ fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # mus_acc) = (map sq_norm (rev gs) @ map sq_norm gs', rev mus @ mus_acc)
 3. (fst (mus_adjuster f n_gs [] (0\<^sub>v n)), snd (mus_adjuster f n_gs [] (0\<^sub>v n))) = mus_adjuster f n_gs [] (0\<^sub>v n)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') \<subseteq> carrier_vec n
[PROOF STEP]
using 2 aw_c
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3 = mus_adjuster f n_gs [] (0\<^sub>v n); (?xa3, ?y3) = ?x3; ?xb3 = ?y3 + f; (?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) ?gs'3; sub2_wit ?gs'3 fs = (?mus3, ?gs3); set fs \<subseteq> carrier_vec n; set ?gs'3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' fs ((?xb3, \<parallel>?xb3\<parallel>\<^sup>2) # n_gs) (?xa3 # mus_acc) = (map sq_norm (rev ?gs3 @ ?gs'3), rev ?mus3 @ ?xa3 # mus_acc)
n_gs = map (\<lambda>v. (v, \<parallel>v\<parallel>\<^sup>2)) gs'
sub2_wit gs' (f # fs) = (mus, gs)
set (f # fs) \<subseteq> carrier_vec n
set gs' \<subseteq> carrier_vec n
snd (mus_adjuster f n_gs [] (0\<^sub>v n)) \<in> carrier_vec n

goal (1 subgoal):
 1. set ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs') \<subseteq> carrier_vec n
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (map sq_norm (rev (tl gs) @ (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs'), rev (tl mus) @ fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # mus_acc) = (map sq_norm (rev gs) @ map sq_norm gs', rev mus @ mus_acc)
 2. (fst (mus_adjuster f n_gs [] (0\<^sub>v n)), snd (mus_adjuster f n_gs [] (0\<^sub>v n))) = mus_adjuster f n_gs [] (0\<^sub>v n)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (fst (mus_adjuster f n_gs [] (0\<^sub>v n)), snd (mus_adjuster f n_gs [] (0\<^sub>v n))) = mus_adjuster f n_gs [] (0\<^sub>v n)
 2. (map sq_norm (rev (tl gs) @ (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs'), rev (tl mus) @ fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # mus_acc) = (map sq_norm (rev gs) @ map sq_norm gs', rev mus @ mus_acc)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map sq_norm (rev (tl gs) @ (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # gs'), rev (tl mus) @ fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # mus_acc) = (map sq_norm (rev gs) @ map sq_norm gs', rev mus @ mus_acc)
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. map sq_norm (rev (tl gs)) @ [\<parallel>snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f\<parallel>\<^sup>2] = map sq_norm (rev gs)
 2. rev (tl mus) @ [fst (mus_adjuster f n_gs [] (0\<^sub>v n))] = rev mus
[PROOF STEP]
using gs
[PROOF STATE]
proof (prove)
using this:
gs = (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # tl gs

goal (2 subgoals):
 1. map sq_norm (rev (tl gs)) @ [\<parallel>snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f\<parallel>\<^sup>2] = map sq_norm (rev gs)
 2. rev (tl mus) @ [fst (mus_adjuster f n_gs [] (0\<^sub>v n))] = rev mus
[PROOF STEP]
apply(subst gs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. gs = (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # tl gs \<Longrightarrow> map sq_norm (rev (tl ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # tl gs))) @ [\<parallel>snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f\<parallel>\<^sup>2] = map sq_norm (rev gs)
 2. rev (tl mus) @ [fst (mus_adjuster f n_gs [] (0\<^sub>v n))] = rev mus
[PROOF STEP]
apply(subst (2) gs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. gs = (snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # tl gs \<Longrightarrow> map sq_norm (rev (tl ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # tl gs))) @ [\<parallel>snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f\<parallel>\<^sup>2] = map sq_norm (rev ((snd (mus_adjuster f n_gs [] (0\<^sub>v n)) + f) # tl gs))
 2. rev (tl mus) @ [fst (mus_adjuster f n_gs [] (0\<^sub>v n))] = rev mus
[PROOF STEP]
apply (metis list.simps(9) rev.simps(2) rev_map)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (tl mus) @ [fst (mus_adjuster f n_gs [] (0\<^sub>v n))] = rev mus
[PROOF STEP]
using mus
[PROOF STATE]
proof (prove)
using this:
mus = fst (mus_adjuster f n_gs [] (0\<^sub>v n)) # tl mus

goal (1 subgoal):
 1. rev (tl mus) @ [fst (mus_adjuster f n_gs [] (0\<^sub>v n))] = rev mus
[PROOF STEP]
by (metis rev.simps(2))
[PROOF STATE]
proof (state)
this:
norms_mus' (f # fs) n_gs mus_acc = (map sq_norm (rev gs @ gs'), rev mus @ mus_acc)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub2_wit_gram_schmidt_sub_triv'':
  assumes "sub2_wit [] fs = (mus, gs)" "set fs \<subseteq> carrier_vec n"
  shows "norms_mus' fs [] [] = (map sq_norm_vec (rev gs), rev mus)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norms_mus' fs [] [] = (map sq_norm (rev gs), rev mus)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sub2_wit [] fs = (mus, gs)
set fs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. norms_mus' fs [] [] = (map sq_norm (rev gs), rev mus)
[PROOF STEP]
by (subst sub2_wit_norms_mus') (simp)+


[STATEMENT]
lemma sub2_wit_gram_schmidt_norm_mus:
  assumes "sub2_wit [] fs = (mus, gs)" "set fs \<subseteq> carrier_vec n"
  shows "norms_mus fs = (map sq_norm_vec gs, mus)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norms_mus fs = (map sq_norm gs, mus)
[PROOF STEP]
unfolding norms_mus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let (n_gs, mus) = norms_mus' fs [] [] in (rev n_gs, rev mus)) = (map sq_norm gs, mus)
[PROOF STEP]
using assms sub2_wit_gram_schmidt_sub_triv''
[PROOF STATE]
proof (prove)
using this:
sub2_wit [] fs = (mus, gs)
set fs \<subseteq> carrier_vec n
\<lbrakk>sub2_wit [] ?fs = (?mus, ?gs); set ?fs \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> norms_mus' ?fs [] [] = (map sq_norm (rev ?gs), rev ?mus)

goal (1 subgoal):
 1. (let (n_gs, mus) = norms_mus' fs [] [] in (rev n_gs, rev mus)) = (map sq_norm gs, mus)
[PROOF STEP]
by (auto simp add: Let_def case_prod_beta' rev_map)


[STATEMENT]
lemma (in gram_schmidt_fs_Rn) norms_mus: assumes "set fs \<subseteq> carrier_vec n" "length fs \<le> n"
  shows "norms_mus fs = (map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<length fs], map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norms_mus fs = (map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<length fs], map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norms_mus fs = (map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<length fs], map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs])
[PROOF STEP]
let ?s = "sub2_wit [] fs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norms_mus fs = (map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<length fs], map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs])
[PROOF STEP]
have "gram_schmidt_sub2 n [] fs = snd ?s \<and> snd ?s = map (gso) [0..<length fs] \<and> fst ?s = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gram_schmidt_sub2 n [] fs = snd (sub2_wit [] fs) \<and> snd (sub2_wit [] fs) = map gso [0..<length fs] \<and> fst (sub2_wit [] fs) = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set fs \<subseteq> carrier_vec n
length fs \<le> n

goal (1 subgoal):
 1. gram_schmidt_sub2 n [] fs = snd (sub2_wit [] fs) \<and> snd (sub2_wit [] fs) = map gso [0..<length fs] \<and> fst (sub2_wit [] fs) = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]
[PROOF STEP]
by (intro sub2_wit) (auto simp add: map_nth)
[PROOF STATE]
proof (state)
this:
gram_schmidt_sub2 n [] fs = snd (sub2_wit [] fs) \<and> snd (sub2_wit [] fs) = map gso [0..<length fs] \<and> fst (sub2_wit [] fs) = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]

goal (1 subgoal):
 1. norms_mus fs = (map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<length fs], map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gram_schmidt_sub2 n [] fs = snd (sub2_wit [] fs) \<and> snd (sub2_wit [] fs) = map gso [0..<length fs] \<and> fst (sub2_wit [] fs) = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]
[PROOF STEP]
have 1: "snd ?s = map (gso) [0..<length fs]" and 2: "fst ?s = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]"
[PROOF STATE]
proof (prove)
using this:
gram_schmidt_sub2 n [] fs = snd (sub2_wit [] fs) \<and> snd (sub2_wit [] fs) = map gso [0..<length fs] \<and> fst (sub2_wit [] fs) = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]

goal (1 subgoal):
 1. snd (sub2_wit [] fs) = map gso [0..<length fs] &&& fst (sub2_wit [] fs) = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd (sub2_wit [] fs) = map gso [0..<length fs]
fst (sub2_wit [] fs) = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]

goal (1 subgoal):
 1. norms_mus fs = (map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<length fs], map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs])
[PROOF STEP]
have s: "?s = (fst ?s, snd ?s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub2_wit [] fs = (fst (sub2_wit [] fs), snd (sub2_wit [] fs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sub2_wit [] fs = (fst (sub2_wit [] fs), snd (sub2_wit [] fs))

goal (1 subgoal):
 1. norms_mus fs = (map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<length fs], map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norms_mus fs = (map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<length fs], map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs])
[PROOF STEP]
unfolding sub2_wit_gram_schmidt_norm_mus[OF s assms(1)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map sq_norm (snd (sub2_wit [] fs)), fst (sub2_wit [] fs)) = (map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<length fs], map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs])
[PROOF STEP]
unfolding 1 2 o_def map_map
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map (\<lambda>x. \<parallel>gso x\<parallel>\<^sup>2) [0..<length fs], map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]) = (map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<length fs], map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
norms_mus fs = (map (\<lambda>j. \<parallel>gso j\<parallel>\<^sup>2) [0..<length fs], map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma norms_mus_rat_norms_mus:
  "norms_mus_rat n fs = gram_schmidt.norms_mus n fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norms_mus_rat n fs = gram_schmidt.norms_mus n fs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norms_mus_rat n fs = gram_schmidt.norms_mus n fs
[PROOF STEP]
have "mus_adjuster_rat f n_gs mus_acc g_acc = gram_schmidt.mus_adjuster f n_gs mus_acc g_acc"
    for f n_gs mus_acc g_acc
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mus_adjuster_rat f n_gs mus_acc g_acc = gram_schmidt.mus_adjuster f n_gs mus_acc g_acc
[PROOF STEP]
by(induction f n_gs mus_acc g_acc rule: mus_adjuster_rat.induct)
      (auto simp add: gram_schmidt.mus_adjuster.simps)
[PROOF STATE]
proof (state)
this:
mus_adjuster_rat ?f ?n_gs ?mus_acc ?g_acc = gram_schmidt.mus_adjuster ?f ?n_gs ?mus_acc ?g_acc

goal (1 subgoal):
 1. norms_mus_rat n fs = gram_schmidt.norms_mus n fs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mus_adjuster_rat ?f ?n_gs ?mus_acc ?g_acc = gram_schmidt.mus_adjuster ?f ?n_gs ?mus_acc ?g_acc
[PROOF STEP]
have "norms_mus_rat' n fs n_gs mus = gram_schmidt.norms_mus' n fs n_gs mus" for n fs n_gs mus
[PROOF STATE]
proof (prove)
using this:
mus_adjuster_rat ?f ?n_gs ?mus_acc ?g_acc = gram_schmidt.mus_adjuster ?f ?n_gs ?mus_acc ?g_acc

goal (1 subgoal):
 1. norms_mus_rat' n fs n_gs mus = gram_schmidt.norms_mus' n fs n_gs mus
[PROOF STEP]
by(induction n fs n_gs mus rule: norms_mus_rat'.induct)
      (auto simp add: gram_schmidt.norms_mus'.simps case_prod_beta')
[PROOF STATE]
proof (state)
this:
norms_mus_rat' ?n ?fs ?n_gs ?mus = gram_schmidt.norms_mus' ?n ?fs ?n_gs ?mus

goal (1 subgoal):
 1. norms_mus_rat n fs = gram_schmidt.norms_mus n fs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
norms_mus_rat' ?n ?fs ?n_gs ?mus = gram_schmidt.norms_mus' ?n ?fs ?n_gs ?mus
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
norms_mus_rat' ?n ?fs ?n_gs ?mus = gram_schmidt.norms_mus' ?n ?fs ?n_gs ?mus

goal (1 subgoal):
 1. norms_mus_rat n fs = gram_schmidt.norms_mus n fs
[PROOF STEP]
unfolding norms_mus_rat_def gram_schmidt.norms_mus_def
[PROOF STATE]
proof (prove)
using this:
norms_mus_rat' ?n ?fs ?n_gs ?mus = gram_schmidt.norms_mus' ?n ?fs ?n_gs ?mus

goal (1 subgoal):
 1. (let (n_gs, mus) = norms_mus_rat' n fs [] [] in (rev n_gs, rev mus)) = (let (n_gs, mus) = gram_schmidt.norms_mus' n fs [] [] in (rev n_gs, rev mus))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
norms_mus_rat n fs = gram_schmidt.norms_mus n fs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_int_dvd:
  "b dvd a" if "of_int a / (of_int b :: 'a :: field_char_0) \<in> \<int>" "b \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b dvd a
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
of_int a / of_int b \<in> \<int>
b \<noteq> 0

goal (1 subgoal):
 1. b dvd a
[PROOF STEP]
by (cases rule: Ints_cases)
    (simp add: field_simps flip: of_int_mult)


[STATEMENT]
lemma denom_dvd_ints:
  fixes i::int
  assumes "quotient_of r = (z, n)" "of_int i * r \<in> \<int>"
  shows "n dvd i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n dvd i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n dvd i
[PROOF STEP]
have "rat_of_int i * (rat_of_int z / rat_of_int n) \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int i * (rat_of_int z / rat_of_int n) \<in> \<int>
[PROOF STEP]
using assms quotient_of_div
[PROOF STATE]
proof (prove)
using this:
quotient_of r = (z, n)
rat_of_int i * r \<in> \<int>
quotient_of ?r = (?n, ?d) \<Longrightarrow> ?r = rat_of_int ?n / rat_of_int ?d

goal (1 subgoal):
 1. rat_of_int i * (rat_of_int z / rat_of_int n) \<in> \<int>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rat_of_int i * (rat_of_int z / rat_of_int n) \<in> \<int>

goal (1 subgoal):
 1. n dvd i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rat_of_int i * (rat_of_int z / rat_of_int n) \<in> \<int>
[PROOF STEP]
have "n dvd i * z"
[PROOF STATE]
proof (prove)
using this:
rat_of_int i * (rat_of_int z / rat_of_int n) \<in> \<int>

goal (1 subgoal):
 1. n dvd i * z
[PROOF STEP]
using quotient_of_denom_pos assms
[PROOF STATE]
proof (prove)
using this:
rat_of_int i * (rat_of_int z / rat_of_int n) \<in> \<int>
quotient_of ?r = (?p, ?q) \<Longrightarrow> 0 < ?q
quotient_of r = (z, n)
rat_of_int i * r \<in> \<int>

goal (1 subgoal):
 1. n dvd i * z
[PROOF STEP]
by (auto intro!: of_int_dvd)
[PROOF STATE]
proof (state)
this:
n dvd i * z

goal (1 subgoal):
 1. n dvd i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n dvd i * z
[PROOF STEP]
show "n dvd i"
[PROOF STATE]
proof (prove)
using this:
n dvd i * z

goal (1 subgoal):
 1. n dvd i
[PROOF STEP]
using assms algebraic_semidom_class.coprime_commute
      quotient_of_coprime coprime_dvd_mult_left_iff
[PROOF STATE]
proof (prove)
using this:
n dvd i * z
quotient_of r = (z, n)
rat_of_int i * r \<in> \<int>
algebraic_semidom_class.coprime ?b ?a = algebraic_semidom_class.coprime ?a ?b
quotient_of ?r = (?p, ?q) \<Longrightarrow> algebraic_semidom_class.coprime ?p ?q
algebraic_semidom_class.coprime ?a ?c \<Longrightarrow> (?a dvd ?b * ?c) = (?a dvd ?b)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quotient_of_bounds:
  assumes "quotient_of r = (n, d)" "rat_of_int i * r \<in> \<int>" "0 < i" "\<bar>r\<bar> \<le> b"
  shows "of_int \<bar>n\<bar> \<le> of_int i * b" "d \<le> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b &&& d \<le> i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b
 2. d \<le> i
[PROOF STEP]
show ni: "d \<le> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<le> i
[PROOF STEP]
using assms denom_dvd_ints
[PROOF STATE]
proof (prove)
using this:
quotient_of r = (n, d)
rat_of_int i * r \<in> \<int>
0 < i
\<bar>r\<bar> \<le> b
\<lbrakk>quotient_of ?r = (?z, ?n); rat_of_int ?i * ?r \<in> \<int>\<rbrakk> \<Longrightarrow> ?n dvd ?i

goal (1 subgoal):
 1. d \<le> i
[PROOF STEP]
by (intro zdvd_imp_le) blast+
[PROOF STATE]
proof (state)
this:
d \<le> i

goal (1 subgoal):
 1. rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b
[PROOF STEP]
have "\<bar>r\<bar> = \<bar>rat_of_int n / rat_of_int d\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>r\<bar> = \<bar>rat_of_int n / rat_of_int d\<bar>
[PROOF STEP]
using assms quotient_of_div
[PROOF STATE]
proof (prove)
using this:
quotient_of r = (n, d)
rat_of_int i * r \<in> \<int>
0 < i
\<bar>r\<bar> \<le> b
quotient_of ?r = (?n, ?d) \<Longrightarrow> ?r = rat_of_int ?n / rat_of_int ?d

goal (1 subgoal):
 1. \<bar>r\<bar> = \<bar>rat_of_int n / rat_of_int d\<bar>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<bar>r\<bar> = \<bar>rat_of_int n / rat_of_int d\<bar>

goal (1 subgoal):
 1. rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>r\<bar> = \<bar>rat_of_int n / rat_of_int d\<bar>

goal (1 subgoal):
 1. rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b
[PROOF STEP]
have "\<dots> = rat_of_int \<bar>n\<bar> / rat_of_int d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>rat_of_int n / rat_of_int d\<bar> = rat_of_int \<bar>n\<bar> / rat_of_int d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
quotient_of r = (n, d)
rat_of_int i * r \<in> \<int>
0 < i
\<bar>r\<bar> \<le> b

goal (1 subgoal):
 1. \<bar>rat_of_int n / rat_of_int d\<bar> = rat_of_int \<bar>n\<bar> / rat_of_int d
[PROOF STEP]
using quotient_of_denom_pos
[PROOF STATE]
proof (prove)
using this:
quotient_of r = (n, d)
rat_of_int i * r \<in> \<int>
0 < i
\<bar>r\<bar> \<le> b
quotient_of ?r = (?p, ?q) \<Longrightarrow> 0 < ?q

goal (1 subgoal):
 1. \<bar>rat_of_int n / rat_of_int d\<bar> = rat_of_int \<bar>n\<bar> / rat_of_int d
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<bar>rat_of_int n / rat_of_int d\<bar> = rat_of_int \<bar>n\<bar> / rat_of_int d

goal (1 subgoal):
 1. rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>r\<bar> = rat_of_int \<bar>n\<bar> / rat_of_int d
[PROOF STEP]
have "of_int \<bar>n\<bar> = rat_of_int d * \<bar>r\<bar>"
[PROOF STATE]
proof (prove)
using this:
\<bar>r\<bar> = rat_of_int \<bar>n\<bar> / rat_of_int d

goal (1 subgoal):
 1. rat_of_int \<bar>n\<bar> = rat_of_int d * \<bar>r\<bar>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<bar>r\<bar> = rat_of_int \<bar>n\<bar> / rat_of_int d
quotient_of r = (n, d)
rat_of_int i * r \<in> \<int>
0 < i
\<bar>r\<bar> \<le> b

goal (1 subgoal):
 1. rat_of_int \<bar>n\<bar> = rat_of_int d * \<bar>r\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rat_of_int \<bar>n\<bar> = rat_of_int d * \<bar>r\<bar>

goal (1 subgoal):
 1. rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rat_of_int \<bar>n\<bar> = rat_of_int d * \<bar>r\<bar>

goal (1 subgoal):
 1. rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b
[PROOF STEP]
have "\<dots> \<le> rat_of_int d * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int d * \<bar>r\<bar> \<le> rat_of_int d * b
[PROOF STEP]
using assms quotient_of_denom_pos
[PROOF STATE]
proof (prove)
using this:
quotient_of r = (n, d)
rat_of_int i * r \<in> \<int>
0 < i
\<bar>r\<bar> \<le> b
quotient_of ?r = (?p, ?q) \<Longrightarrow> 0 < ?q

goal (1 subgoal):
 1. rat_of_int d * \<bar>r\<bar> \<le> rat_of_int d * b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rat_of_int d * \<bar>r\<bar> \<le> rat_of_int d * b

goal (1 subgoal):
 1. rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rat_of_int d * \<bar>r\<bar> \<le> rat_of_int d * b

goal (1 subgoal):
 1. rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b
[PROOF STEP]
have "\<dots> \<le> rat_of_int i * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rat_of_int d * b \<le> rat_of_int i * b
[PROOF STEP]
using ni assms of_int_le_iff
[PROOF STATE]
proof (prove)
using this:
d \<le> i
quotient_of r = (n, d)
rat_of_int i * r \<in> \<int>
0 < i
\<bar>r\<bar> \<le> b
(of_int ?w \<le> of_int ?z) = (?w \<le> ?z)

goal (1 subgoal):
 1. rat_of_int d * b \<le> rat_of_int i * b
[PROOF STEP]
by (auto intro!: mult_right_mono)
[PROOF STATE]
proof (state)
this:
rat_of_int d * b \<le> rat_of_int i * b

goal (1 subgoal):
 1. rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b
[PROOF STEP]
show "rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b"
[PROOF STATE]
proof (prove)
using this:
rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b

goal (1 subgoal):
 1. rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rat_of_int \<bar>n\<bar> \<le> rat_of_int i * b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ex_\<kappa>:
  assumes "i < length fs" "l \<le> i"
  shows "\<exists>\<kappa>. sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0 ..< l]) =
             sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0 ..< l])" (is "\<exists>\<kappa>. ?Prop l i \<kappa>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < length fs
l \<le> i

goal (1 subgoal):
 1. \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
proof (induction l arbitrary: i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < length fs; 0 \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<0]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<0])
 2. \<And>l i. \<lbrakk>\<And>i. \<lbrakk>i < length fs; l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l]); i < length fs; Suc l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i1 < length fs; l \<le> ?i1\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> ?i1 j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l])
i < length fs
Suc l \<le> i

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < length fs; 0 \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<0]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<0])
 2. \<And>l i. \<lbrakk>\<And>i. \<lbrakk>i < length fs; l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l]); i < length fs; Suc l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i1 < length fs; l \<le> ?i1\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> ?i1 j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l])
i < length fs
Suc l \<le> i
[PROOF STEP]
obtain \<kappa>\<^sub>i where \<kappa>\<^sub>i_def: "?Prop l i \<kappa>\<^sub>i"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i1 < length fs; l \<le> ?i1\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> ?i1 j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l])
i < length fs
Suc l \<le> i

goal (1 subgoal):
 1. (\<And>\<kappa>\<^sub>i. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l])

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < length fs; 0 \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<0]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<0])
 2. \<And>l i. \<lbrakk>\<And>i. \<lbrakk>i < length fs; l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l]); i < length fs; Suc l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
from Suc
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i1 < length fs; l \<le> ?i1\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> ?i1 j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l])
i < length fs
Suc l \<le> i
[PROOF STEP]
obtain \<kappa>\<^sub>l where \<kappa>\<^sub>l_def: "?Prop l l \<kappa>\<^sub>l"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i1 < length fs; l \<le> ?i1\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> ?i1 j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l])
i < length fs
Suc l \<le> i

goal (1 subgoal):
 1. (\<And>\<kappa>\<^sub>l. M.sumlist (map (\<lambda>j. - \<mu> l j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. - \<mu> l j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l])

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < length fs; 0 \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<0]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<0])
 2. \<And>l i. \<lbrakk>\<And>i. \<lbrakk>i < length fs; l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l]); i < length fs; Suc l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
have [simp]: "dim_vec (M.sumlist (map (\<lambda>j. f j \<cdot>\<^sub>v fs ! j) [0..<y])) = n" if "y \<le> Suc l" for f y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (M.sumlist (map (\<lambda>j. f j \<cdot>\<^sub>v fs ! j) [0..<y])) = n
[PROOF STEP]
using Suc that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i1 < length fs; l \<le> ?i1\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> ?i1 j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l])
i < length fs
Suc l \<le> i
y \<le> Suc l

goal (1 subgoal):
 1. dim_vec (M.sumlist (map (\<lambda>j. f j \<cdot>\<^sub>v fs ! j) [0..<y])) = n
[PROOF STEP]
by (auto intro!: dim_sumlist)
[PROOF STATE]
proof (state)
this:
?y1 \<le> Suc l \<Longrightarrow> dim_vec (M.sumlist (map (\<lambda>j. ?f1 j \<cdot>\<^sub>v fs ! j) [0..<?y1])) = n

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < length fs; 0 \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<0]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<0])
 2. \<And>l i. \<lbrakk>\<And>i. \<lbrakk>i < length fs; l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l]); i < length fs; Suc l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
define \<kappa> where "\<kappa> = (\<lambda>x. (if x < l then \<kappa>\<^sub>i x - \<kappa>\<^sub>l x * \<mu> i l else  - \<mu> i l))"
[PROOF STATE]
proof (state)
this:
\<kappa> = (\<lambda>x. if x < l then \<kappa>\<^sub>i x - \<kappa>\<^sub>l x * \<mu> i l else - \<mu> i l)

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < length fs; 0 \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<0]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<0])
 2. \<And>l i. \<lbrakk>\<And>i. \<lbrakk>i < length fs; l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l]); i < length fs; Suc l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
let ?sum = "\<lambda>i. sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l])"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < length fs; 0 \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<0]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<0])
 2. \<And>l i. \<lbrakk>\<And>i. \<lbrakk>i < length fs; l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l]); i < length fs; Suc l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
have "M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) =
        M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v gso l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v gso l
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i1 < length fs; l \<le> ?i1\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> ?i1 j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l])
i < length fs
Suc l \<le> i

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v gso l
[PROOF STEP]
by (subst \<kappa>\<^sub>i_def[symmetric], subst sumlist_snoc[symmetric]) (auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v gso l

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < length fs; 0 \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<0]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<0])
 2. \<And>l i. \<lbrakk>\<And>i. \<lbrakk>i < length fs; l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l]); i < length fs; Suc l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v gso l

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < length fs; 0 \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<0]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<0])
 2. \<And>l i. \<lbrakk>\<And>i. \<lbrakk>i < length fs; l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l]); i < length fs; Suc l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
have "gso l = fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso l = fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l])
[PROOF STEP]
by (subst gso.simps) (auto simp add: \<kappa>\<^sub>l_def)
[PROOF STATE]
proof (state)
this:
gso l = fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l])

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < length fs; 0 \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<0]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<0])
 2. \<And>l i. \<lbrakk>\<And>i. \<lbrakk>i < length fs; l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l]); i < length fs; Suc l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gso l = fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l])

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < length fs; 0 \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<0]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<0])
 2. \<And>l i. \<lbrakk>\<And>i. \<lbrakk>i < length fs; l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l]); i < length fs; Suc l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
have "M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) +
             - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))
             = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l])) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l])) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
have "?lhs $ k = ?rhs $ k" if "k < n" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
have "(M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) +
                - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k
          = (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k +
                - \<mu> i l * (fs ! l $ k + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k + - \<mu> i l * (fs ! l $ k + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
k < n

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k + - \<mu> i l * (fs ! l $ k + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k + - \<mu> i l * (fs ! l $ k + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k)

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k + - \<mu> i l * (fs ! l $ k + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k)

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
have "\<dots> = (\<Sum>j = 0..<l. \<kappa>\<^sub>i j * fs ! j $ k)
                 + (- \<mu> i l * (\<Sum>j = 0..<l. \<kappa>\<^sub>l j * fs ! j $ k)) - \<mu> i l * fs ! l $ k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k + - \<mu> i l * (fs ! l $ k + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k) = (\<Sum>j = 0..<l. \<kappa>\<^sub>i j * fs ! j $ k) + - \<mu> i l * (\<Sum>j = 0..<l. \<kappa>\<^sub>l j * fs ! j $ k) - \<mu> i l * fs ! l $ k
[PROOF STEP]
using that Suc
[PROOF STATE]
proof (prove)
using this:
k < n
\<lbrakk>?i1 < length fs; l \<le> ?i1\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> ?i1 j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l])
i < length fs
Suc l \<le> i

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k + - \<mu> i l * (fs ! l $ k + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k) = (\<Sum>j = 0..<l. \<kappa>\<^sub>i j * fs ! j $ k) + - \<mu> i l * (\<Sum>j = 0..<l. \<kappa>\<^sub>l j * fs ! j $ k) - \<mu> i l * fs ! l $ k
[PROOF STEP]
by (auto simp add: algebra_simps sumlist_nth)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k + - \<mu> i l * (fs ! l $ k + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k) = (\<Sum>j = 0..<l. \<kappa>\<^sub>i j * fs ! j $ k) + - \<mu> i l * (\<Sum>j = 0..<l. \<kappa>\<^sub>l j * fs ! j $ k) - \<mu> i l * fs ! l $ k

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k + - \<mu> i l * (fs ! l $ k + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]) $ k) = (\<Sum>j = 0..<l. \<kappa>\<^sub>i j * fs ! j $ k) + - \<mu> i l * (\<Sum>j = 0..<l. \<kappa>\<^sub>l j * fs ! j $ k) - \<mu> i l * fs ! l $ k

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
have "- \<mu> i l * (\<Sum>j = 0..<l. \<kappa>\<^sub>l j * fs ! j $ k)
               = (\<Sum>j = 0..<l. - \<mu> i l * (\<kappa>\<^sub>l j * fs ! j $ k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - \<mu> i l * (\<Sum>j = 0..<l. \<kappa>\<^sub>l j * fs ! j $ k) = (\<Sum>j = 0..<l. - \<mu> i l * (\<kappa>\<^sub>l j * fs ! j $ k))
[PROOF STEP]
using sum_distrib_left
[PROOF STATE]
proof (prove)
using this:
?r * sum ?f ?A = (\<Sum>n\<in>?A. ?r * ?f n)

goal (1 subgoal):
 1. - \<mu> i l * (\<Sum>j = 0..<l. \<kappa>\<^sub>l j * fs ! j $ k) = (\<Sum>j = 0..<l. - \<mu> i l * (\<kappa>\<^sub>l j * fs ! j $ k))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- \<mu> i l * (\<Sum>j = 0..<l. \<kappa>\<^sub>l j * fs ! j $ k) = (\<Sum>j = 0..<l. - \<mu> i l * (\<kappa>\<^sub>l j * fs ! j $ k))

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- \<mu> i l * (\<Sum>j = 0..<l. \<kappa>\<^sub>l j * fs ! j $ k) = (\<Sum>j = 0..<l. - \<mu> i l * (\<kappa>\<^sub>l j * fs ! j $ k))

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
have "(\<Sum>j = 0..<l. \<kappa>\<^sub>i j * fs ! j $ k) + (\<Sum>j = 0..<l. - \<mu> i l * (\<kappa>\<^sub>l j * fs ! j $ k)) =
               (\<Sum>x = 0..<l. (\<kappa>\<^sub>i x - \<kappa>\<^sub>l x * \<mu> i l) * fs ! x $ k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..<l. \<kappa>\<^sub>i j * fs ! j $ k) + (\<Sum>j = 0..<l. - \<mu> i l * (\<kappa>\<^sub>l j * fs ! j $ k)) = (\<Sum>x = 0..<l. (\<kappa>\<^sub>i x - \<kappa>\<^sub>l x * \<mu> i l) * fs ! x $ k)
[PROOF STEP]
by (subst sum.distrib[symmetric]) (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..<l. \<kappa>\<^sub>i j * fs ! j $ k) + (\<Sum>j = 0..<l. - \<mu> i l * (\<kappa>\<^sub>l j * fs ! j $ k)) = (\<Sum>x = 0..<l. (\<kappa>\<^sub>i x - \<kappa>\<^sub>l x * \<mu> i l) * fs ! x $ k)

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..<l. \<kappa>\<^sub>i j * fs ! j $ k) + (\<Sum>j = 0..<l. - \<mu> i l * (\<kappa>\<^sub>l j * fs ! j $ k)) = (\<Sum>x = 0..<l. (\<kappa>\<^sub>i x - \<kappa>\<^sub>l x * \<mu> i l) * fs ! x $ k)

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
have "\<dots> = (\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x = 0..<l. (\<kappa>\<^sub>i x - \<kappa>\<^sub>l x * \<mu> i l) * fs ! x $ k) = (\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k)
[PROOF STEP]
unfolding \<kappa>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x = 0..<l. (\<kappa>\<^sub>i x - \<kappa>\<^sub>l x * \<mu> i l) * fs ! x $ k) = (\<Sum>x = 0..<l. (if x < l then \<kappa>\<^sub>i x - \<kappa>\<^sub>l x * \<mu> i l else - \<mu> i l) * fs ! x $ k)
[PROOF STEP]
by (rule sum.cong) (auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>x = 0..<l. (\<kappa>\<^sub>i x - \<kappa>\<^sub>l x * \<mu> i l) * fs ! x $ k) = (\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k)

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x = 0..<l. (\<kappa>\<^sub>i x - \<kappa>\<^sub>l x * \<mu> i l) * fs ! x $ k) = (\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k)

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
have "(\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k) - \<mu> i l * fs ! l $ k =
                 (\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k) + (\<Sum>x = l..<Suc l. \<kappa> x * fs ! x $ k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k) - \<mu> i l * fs ! l $ k = (\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k) + (\<Sum>x = l..<Suc l. \<kappa> x * fs ! x $ k)
[PROOF STEP]
unfolding \<kappa>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x = 0..<l. (if x < l then \<kappa>\<^sub>i x - \<kappa>\<^sub>l x * \<mu> i l else - \<mu> i l) * fs ! x $ k) - \<mu> i l * fs ! l $ k = (\<Sum>x = 0..<l. (if x < l then \<kappa>\<^sub>i x - \<kappa>\<^sub>l x * \<mu> i l else - \<mu> i l) * fs ! x $ k) + (\<Sum>x = l..<Suc l. (if x < l then \<kappa>\<^sub>i x - \<kappa>\<^sub>l x * \<mu> i l else - \<mu> i l) * fs ! x $ k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k) - \<mu> i l * fs ! l $ k = (\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k) + (\<Sum>x = l..<Suc l. \<kappa> x * fs ! x $ k)

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k) - \<mu> i l * fs ! l $ k = (\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k) + (\<Sum>x = l..<Suc l. \<kappa> x * fs ! x $ k)

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
have "\<dots> = (\<Sum>x = 0..<Suc l. \<kappa> x * fs ! x $ k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k) + (\<Sum>x = l..<Suc l. \<kappa> x * fs ! x $ k) = (\<Sum>x = 0..<Suc l. \<kappa> x * fs ! x $ k)
[PROOF STEP]
by (subst sum.union_disjoint[symmetric]) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k) + (\<Sum>x = l..<Suc l. \<kappa> x * fs ! x $ k) = (\<Sum>x = 0..<Suc l. \<kappa> x * fs ! x $ k)

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x = 0..<l. \<kappa> x * fs ! x $ k) + (\<Sum>x = l..<Suc l. \<kappa> x * fs ! x $ k) = (\<Sum>x = 0..<Suc l. \<kappa> x * fs ! x $ k)

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
have "\<dots> = (\<Sum>x = 0..<Suc l. (\<kappa> x \<cdot>\<^sub>v fs ! x) $ k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x = 0..<Suc l. \<kappa> x * fs ! x $ k) = (\<Sum>x = 0..<Suc l. (\<kappa> x \<cdot>\<^sub>v fs ! x) $ k)
[PROOF STEP]
using that Suc
[PROOF STATE]
proof (prove)
using this:
k < n
\<lbrakk>?i1 < length fs; l \<le> ?i1\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> ?i1 j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l])
i < length fs
Suc l \<le> i

goal (1 subgoal):
 1. (\<Sum>x = 0..<Suc l. \<kappa> x * fs ! x $ k) = (\<Sum>x = 0..<Suc l. (\<kappa> x \<cdot>\<^sub>v fs ! x) $ k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x = 0..<Suc l. \<kappa> x * fs ! x $ k) = (\<Sum>x = 0..<Suc l. (\<kappa> x \<cdot>\<^sub>v fs ! x) $ k)

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x = 0..<Suc l. \<kappa> x * fs ! x $ k) = (\<Sum>x = 0..<Suc l. (\<kappa> x \<cdot>\<^sub>v fs ! x) $ k)

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
have "\<dots> = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x = 0..<Suc l. (\<kappa> x \<cdot>\<^sub>v fs ! x) $ k) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
by (subst sumlist_nth, insert that Suc, auto simp: nth_append)
[PROOF STATE]
proof (state)
this:
(\<Sum>x = 0..<Suc l. (\<kappa> x \<cdot>\<^sub>v fs ! x) $ k) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k

goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ k = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?k1 < n \<Longrightarrow> (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ ?k1 = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ ?k1

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l])) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k1 < n \<Longrightarrow> (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ ?k1 = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ ?k1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?k1 < n \<Longrightarrow> (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ ?k1 = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ ?k1

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l])) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
?k1 < n \<Longrightarrow> (M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l]))) $ ?k1 = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l]) $ ?k1
\<lbrakk>?i1 < length fs; l \<le> ?i1\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> ?i1 j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l])
i < length fs
Suc l \<le> i

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l])) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
by (auto simp add: dim_sumlist)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l])) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<kappa>\<^sub>i j \<cdot>\<^sub>v fs ! j) [0..<l]) + - \<mu> i l \<cdot>\<^sub>v (fs ! l + M.sumlist (map (\<lambda>j. \<kappa>\<^sub>l j \<cdot>\<^sub>v fs ! j) [0..<l])) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < length fs; 0 \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<0]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<0])
 2. \<And>l i. \<lbrakk>\<And>i. \<lbrakk>i < length fs; l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<l]); i < length fs; Suc l \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])

goal (1 subgoal):
 1. \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])
[PROOF STEP]
by (intro exI[of _ \<kappa>]) simp
[PROOF STATE]
proof (state)
this:
\<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc l]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<Suc l])

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < length fs; 0 \<le> i\<rbrakk> \<Longrightarrow> \<exists>\<kappa>. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<0]) = M.sumlist (map (\<lambda>j. \<kappa> j \<cdot>\<^sub>v fs ! j) [0..<0])
[PROOF STEP]
qed auto