[STATEMENT]
lemma gauss_jordan_row_echelon:
  assumes A: "A \<in> carrier_mat nr nc"
  and res: "gauss_jordan A B = (A', B')"
  shows "row_echelon_form A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
by (rule gauss_jordan_main_row_echelon[OF A res[unfolded gauss_jordan_def] pivot_fun_init], auto)


[STATEMENT]
lemma pivot_bound: assumes dim: "dim_row A = nr"
  and pivot: "pivot_fun A f n"
  shows "i + j < nr \<Longrightarrow> f (i + j) = n \<or> f (i + j) \<ge> j + f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + j < nr \<Longrightarrow> f (i + j) = n \<or> j + f i \<le> f (i + j)
[PROOF STEP]
proof (induct j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i + 0 < nr \<Longrightarrow> f (i + 0) = n \<or> 0 + f i \<le> f (i + 0)
 2. \<And>j. \<lbrakk>i + j < nr \<Longrightarrow> f (i + j) = n \<or> j + f i \<le> f (i + j); i + Suc j < nr\<rbrakk> \<Longrightarrow> f (i + Suc j) = n \<or> Suc j + f i \<le> f (i + Suc j)
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
i + j < nr \<Longrightarrow> f (i + j) = n \<or> j + f i \<le> f (i + j)
i + Suc j < nr

goal (2 subgoals):
 1. i + 0 < nr \<Longrightarrow> f (i + 0) = n \<or> 0 + f i \<le> f (i + 0)
 2. \<And>j. \<lbrakk>i + j < nr \<Longrightarrow> f (i + j) = n \<or> j + f i \<le> f (i + j); i + Suc j < nr\<rbrakk> \<Longrightarrow> f (i + Suc j) = n \<or> Suc j + f i \<le> f (i + Suc j)
[PROOF STEP]
hence IH: "f (i + j) = n \<or> j + f i \<le> f (i + j)"
    and lt: "i + j < nr" "Suc (i + j) < nr"
[PROOF STATE]
proof (prove)
using this:
i + j < nr \<Longrightarrow> f (i + j) = n \<or> j + f i \<le> f (i + j)
i + Suc j < nr

goal (1 subgoal):
 1. f (i + j) = n \<or> j + f i \<le> f (i + j) &&& i + j < nr &&& Suc (i + j) < nr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (i + j) = n \<or> j + f i \<le> f (i + j)
i + j < nr
Suc (i + j) < nr

goal (2 subgoals):
 1. i + 0 < nr \<Longrightarrow> f (i + 0) = n \<or> 0 + f i \<le> f (i + 0)
 2. \<And>j. \<lbrakk>i + j < nr \<Longrightarrow> f (i + j) = n \<or> j + f i \<le> f (i + j); i + Suc j < nr\<rbrakk> \<Longrightarrow> f (i + Suc j) = n \<or> Suc j + f i \<le> f (i + Suc j)
[PROOF STEP]
note p = pivot_funD[OF dim pivot]
[PROOF STATE]
proof (state)
this:
?i < nr \<Longrightarrow> f ?i \<le> n
\<lbrakk>?i < nr; ?j < f ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> f ?i < f (Suc ?i) \<or> f (Suc ?i) = n
\<lbrakk>?i < nr; f ?i < n\<rbrakk> \<Longrightarrow> A $$ (?i, f ?i) = (1::'a)
\<lbrakk>?i < nr; f ?i < n; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', f ?i) = (0::'a)

goal (2 subgoals):
 1. i + 0 < nr \<Longrightarrow> f (i + 0) = n \<or> 0 + f i \<le> f (i + 0)
 2. \<And>j. \<lbrakk>i + j < nr \<Longrightarrow> f (i + j) = n \<or> j + f i \<le> f (i + j); i + Suc j < nr\<rbrakk> \<Longrightarrow> f (i + Suc j) = n \<or> Suc j + f i \<le> f (i + Suc j)
[PROOF STEP]
from p(3)[OF lt] IH p(1)[OF lt(2)]
[PROOF STATE]
proof (chain)
picking this:
f (i + j) < f (Suc (i + j)) \<or> f (Suc (i + j)) = n
f (i + j) = n \<or> j + f i \<le> f (i + j)
f (Suc (i + j)) \<le> n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
f (i + j) < f (Suc (i + j)) \<or> f (Suc (i + j)) = n
f (i + j) = n \<or> j + f i \<le> f (i + j)
f (Suc (i + j)) \<le> n

goal (1 subgoal):
 1. f (i + Suc j) = n \<or> Suc j + f i \<le> f (i + Suc j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (i + Suc j) = n \<or> Suc j + f i \<le> f (i + Suc j)

goal (1 subgoal):
 1. i + 0 < nr \<Longrightarrow> f (i + 0) = n \<or> 0 + f i \<le> f (i + 0)
[PROOF STEP]
qed simp


[STATEMENT]
lemma pivot_positions_main: assumes A: "A \<in> carrier_mat nr nc"
  and pivot: "pivot_fun A f nc"
  shows "j \<le> f i \<or> i \<ge> nr \<Longrightarrow>
    set (pivot_positions_main i j) = {(i', f i') | i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc}
    \<and> distinct (map snd (pivot_positions_main i j))
    \<and> distinct (map fst (pivot_positions_main i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<le> f i \<or> nr \<le> i \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
proof (induct i j rule: pivot_positions_main_gen.induct[of nr nc A 0])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<lbrakk>i < nr; j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j))); \<lbrakk>i < nr; j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j))); j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
case (1 i j)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < nr; j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j)))
\<lbrakk>i < nr; j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j)))
j \<le> f i \<or> nr \<le> i

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<lbrakk>i < nr; j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j))); \<lbrakk>i < nr; j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j))); j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
let ?a = "A $$ (i,j)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<lbrakk>i < nr; j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j))); \<lbrakk>i < nr; j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j))); j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
let ?pivot = "\<lambda> i j. pivot_positions_main i j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<lbrakk>i < nr; j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j))); \<lbrakk>i < nr; j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j))); j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
let ?set = "\<lambda> i. {(i',f i') | i'. i \<le> i' \<and> i' < nr}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<lbrakk>i < nr; j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j))); \<lbrakk>i < nr; j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j))); j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
let ?s = "?set i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<lbrakk>i < nr; j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j))); \<lbrakk>i < nr; j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j))); j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
let ?set = "\<lambda> i. {(i',f i') | i'. i \<le> i' \<and> i' < nr}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<lbrakk>i < nr; j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j))); \<lbrakk>i < nr; j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j))); j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
let ?s = "?set i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<lbrakk>i < nr; j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j))); \<lbrakk>i < nr; j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j))); j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
let ?p = "?pivot i j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<lbrakk>i < nr; j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j))); \<lbrakk>i < nr; j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j))); j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat nr nc
[PROOF STEP]
have dA: "dim_row A = nr"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. dim_row A = nr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_row A = nr

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<lbrakk>i < nr; j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j))); \<lbrakk>i < nr; j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j))); j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
note [simp] = pivot_positions_main_gen.simps[of 0 A nr nc i j]
[PROOF STATE]
proof (state)
this:
local.pivot_positions_main i j = (if i < nr then if j < nc then if A $$ (i, j) = (0::'a) then local.pivot_positions_main i (Suc j) else (i, j) # local.pivot_positions_main (Suc i) (Suc j) else [] else [])

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<lbrakk>i < nr; j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j))); \<lbrakk>i < nr; j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j))); j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
proof (cases "i < nr")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. \<not> i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < nr

goal (2 subgoals):
 1. i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. \<not> i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
note i = this
[PROOF STATE]
proof (state)
this:
i < nr

goal (2 subgoals):
 1. i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. \<not> i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
note IH = 1(1-2)[OF True]
[PROOF STATE]
proof (state)
this:
\<lbrakk>j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j)))
\<lbrakk>j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j)))

goal (2 subgoals):
 1. i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. \<not> i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
have jfi: "j \<le> f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<le> f i
[PROOF STEP]
using 1(3) i
[PROOF STATE]
proof (prove)
using this:
j \<le> f i \<or> nr \<le> i
i < nr

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

goal (2 subgoals):
 1. i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. \<not> i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
note pivotB = pivot_bound[OF dA pivot]
[PROOF STATE]
proof (state)
this:
?i + ?j < nr \<Longrightarrow> f (?i + ?j) = nc \<or> ?j + f ?i \<le> f (?i + ?j)

goal (2 subgoals):
 1. i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. \<not> i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
note pivot' = pivot_funD[OF dA pivot]
[PROOF STATE]
proof (state)
this:
?i < nr \<Longrightarrow> f ?i \<le> nc
\<lbrakk>?i < nr; ?j < f ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> f ?i < f (Suc ?i) \<or> f (Suc ?i) = nc
\<lbrakk>?i < nr; f ?i < nc\<rbrakk> \<Longrightarrow> A $$ (?i, f ?i) = (1::'a)
\<lbrakk>?i < nr; f ?i < nc; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', f ?i) = (0::'a)

goal (2 subgoals):
 1. i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. \<not> i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
note pivot = pivot'[OF True]
[PROOF STATE]
proof (state)
this:
f i \<le> nc
?j < f i \<Longrightarrow> A $$ (i, ?j) = (0::'a)
Suc i < nr \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc
f i < nc \<Longrightarrow> A $$ (i, f i) = (1::'a)
\<lbrakk>f i < nc; ?i' < nr; ?i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (?i', f i) = (0::'a)

goal (2 subgoals):
 1. i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. \<not> i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
have id1: "[i ..< nr] = i # [Suc i ..< nr]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [i..<nr] = i # [Suc i..<nr]
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < nr

goal (1 subgoal):
 1. [i..<nr] = i # [Suc i..<nr]
[PROOF STEP]
by (rule upt_conv_Cons)
[PROOF STATE]
proof (state)
this:
[i..<nr] = i # [Suc i..<nr]

goal (2 subgoals):
 1. i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. \<not> i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
proof (cases "j < nc")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
j < nc

goal (2 subgoals):
 1. j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
note j = this
[PROOF STATE]
proof (state)
this:
j < nc

goal (2 subgoals):
 1. j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
note IH = IH(1-2)[OF True]
[PROOF STATE]
proof (state)
this:
\<lbrakk>A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j)))
\<lbrakk>A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j)))

goal (2 subgoals):
 1. j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
proof (cases "?a = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A $$ (i, j) = (0::'a)

goal (2 subgoals):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
note a = this
[PROOF STATE]
proof (state)
this:
A $$ (i, j) = (0::'a)

goal (2 subgoals):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
from i j a
[PROOF STATE]
proof (chain)
picking this:
i < nr
j < nc
A $$ (i, j) = (0::'a)
[PROOF STEP]
have p: "?p = ?pivot i (Suc j)"
[PROOF STATE]
proof (prove)
using this:
i < nr
j < nc
A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. local.pivot_positions_main i j = local.pivot_positions_main i (Suc j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.pivot_positions_main i j = local.pivot_positions_main i (Suc j)

goal (2 subgoals):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
local.pivot_positions_main i j = local.pivot_positions_main i (Suc j)

goal (2 subgoals):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
assume "f i = j"
[PROOF STATE]
proof (state)
this:
f i = j

goal (2 subgoals):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
with pivot(4) j
[PROOF STATE]
proof (chain)
picking this:
f i < nc \<Longrightarrow> A $$ (i, f i) = (1::'a)
j < nc
f i = j
[PROOF STEP]
have "?a = 1"
[PROOF STATE]
proof (prove)
using this:
f i < nc \<Longrightarrow> A $$ (i, f i) = (1::'a)
j < nc
f i = j

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

goal (2 subgoals):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
with a
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, j) = (0::'a)
A $$ (i, j) = (1::'a)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
A $$ (i, j) = (0::'a)
A $$ (i, j) = (1::'a)

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

goal (2 subgoals):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
f i = j \<Longrightarrow> False

goal (2 subgoals):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
with jfi
[PROOF STATE]
proof (chain)
picking this:
j \<le> f i
f i = j \<Longrightarrow> False
[PROOF STEP]
have "Suc j \<le> f i \<or> i \<ge> nr"
[PROOF STATE]
proof (prove)
using this:
j \<le> f i
f i = j \<Longrightarrow> False

goal (1 subgoal):
 1. Suc j \<le> f i \<or> nr \<le> i
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Suc j \<le> f i \<or> nr \<le> i

goal (2 subgoals):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
note IH = IH(1)[OF True this]
[PROOF STATE]
proof (state)
this:
set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j)))

goal (2 subgoals):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j)))

goal (1 subgoal):
 1. set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
unfolding p
[PROOF STATE]
proof (prove)
using this:
set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j)))

goal (1 subgoal):
 1. set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))

goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
A $$ (i, j) \<noteq> (0::'a)

goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
note a = this
[PROOF STATE]
proof (state)
this:
A $$ (i, j) \<noteq> (0::'a)

goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
from i j a
[PROOF STATE]
proof (chain)
picking this:
i < nr
j < nc
A $$ (i, j) \<noteq> (0::'a)
[PROOF STEP]
have p: "?p = (i,j) # ?pivot (Suc i) (Suc j)"
[PROOF STATE]
proof (prove)
using this:
i < nr
j < nc
A $$ (i, j) \<noteq> (0::'a)

goal (1 subgoal):
 1. local.pivot_positions_main i j = (i, j) # local.pivot_positions_main (Suc i) (Suc j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.pivot_positions_main i j = (i, j) # local.pivot_positions_main (Suc i) (Suc j)

goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
from pivot(2)[of j] jfi a
[PROOF STATE]
proof (chain)
picking this:
j < f i \<Longrightarrow> A $$ (i, j) = (0::'a)
j \<le> f i
A $$ (i, j) \<noteq> (0::'a)
[PROOF STEP]
have jfi: "j = f i"
[PROOF STATE]
proof (prove)
using this:
j < f i \<Longrightarrow> A $$ (i, j) = (0::'a)
j \<le> f i
A $$ (i, j) \<noteq> (0::'a)

goal (1 subgoal):
 1. j = f i
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
j = f i

goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
from pivotB[of i "Suc 0"] jfi
[PROOF STATE]
proof (chain)
picking this:
i + Suc 0 < nr \<Longrightarrow> f (i + Suc 0) = nc \<or> Suc 0 + f i \<le> f (i + Suc 0)
j = f i
[PROOF STEP]
have "Suc j \<le> f (Suc i) \<or> nr \<le> Suc i"
[PROOF STATE]
proof (prove)
using this:
i + Suc 0 < nr \<Longrightarrow> f (i + Suc 0) = nc \<or> Suc 0 + f i \<le> f (i + Suc 0)
j = f i

goal (1 subgoal):
 1. Suc j \<le> f (Suc i) \<or> nr \<le> Suc i
[PROOF STEP]
using Suc_le_eq j leI
[PROOF STATE]
proof (prove)
using this:
i + Suc 0 < nr \<Longrightarrow> f (i + Suc 0) = nc \<or> Suc 0 + f i \<le> f (i + Suc 0)
j = f i
(Suc ?m \<le> ?n) = (?m < ?n)
j < nc
\<not> ?x < ?y \<Longrightarrow> ?y \<le> ?x

goal (1 subgoal):
 1. Suc j \<le> f (Suc i) \<or> nr \<le> Suc i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc j \<le> f (Suc i) \<or> nr \<le> Suc i

goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
note IH = IH(2)[OF False this]
[PROOF STATE]
proof (state)
this:
set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j)))

goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j)))

goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
fix i'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
assume *: "f i = f i'" "Suc i \<le> i'" "i' < nr"
[PROOF STATE]
proof (state)
this:
f i = f i'
Suc i \<le> i'
i' < nr

goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
hence "i + (i' - i) = i'"
[PROOF STATE]
proof (prove)
using this:
f i = f i'
Suc i \<le> i'
i' < nr

goal (1 subgoal):
 1. i + (i' - i) = i'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i + (i' - i) = i'

goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
from pivotB[of i "i' - i", unfolded this] * jfi j
[PROOF STATE]
proof (chain)
picking this:
i' < nr \<Longrightarrow> f i' = nc \<or> i' - i + f i \<le> f i'
f i = f i'
Suc i \<le> i'
i' < nr
j = f i
j < nc
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
i' < nr \<Longrightarrow> f i' = nc \<or> i' - i + f i \<le> f i'
f i = f i'
Suc i \<le> i'
i' < nr
j = f i
j < nc

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

goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>f i = f ?i'2; Suc i \<le> ?i'2; ?i'2 < nr\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
note distinct = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>f i = f ?i'2; Suc i \<le> ?i'2; ?i'2 < nr\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
have id2: "?s = insert (i,j) (?set (Suc i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(i', f i') |i'. i \<le> i' \<and> i' < nr} = insert (i, j) {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr}
[PROOF STEP]
using i jfi not_less_eq_eq
[PROOF STATE]
proof (prove)
using this:
i < nr
j = f i
(\<not> ?m \<le> ?n) = (Suc ?n \<le> ?m)

goal (1 subgoal):
 1. {(i', f i') |i'. i \<le> i' \<and> i' < nr} = insert (i, j) {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
{(i', f i') |i'. i \<le> i' \<and> i' < nr} = insert (i, j) {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr}

goal (1 subgoal):
 1. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
using IH j jfi i
[PROOF STATE]
proof (prove)
using this:
set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j)))
j < nc
j = f i
i < nr

goal (1 subgoal):
 1. set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
unfolding p id1 id2
[PROOF STATE]
proof (prove)
using this:
set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j)))
j < nc
j = f i
i < nr

goal (1 subgoal):
 1. set ((i, j) # local.pivot_positions_main (Suc i) (Suc j)) = insert (i, j) {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd ((i, j) # local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst ((i, j) # local.pivot_positions_main (Suc i) (Suc j)))
[PROOF STEP]
by (auto intro: distinct)
[PROOF STATE]
proof (state)
this:
set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))

goal (1 subgoal):
 1. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> j < nc

goal (1 subgoal):
 1. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
note j = this
[PROOF STATE]
proof (state)
this:
\<not> j < nc

goal (1 subgoal):
 1. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
from pivot(1) j jfi
[PROOF STATE]
proof (chain)
picking this:
f i \<le> nc
\<not> j < nc
j \<le> f i
[PROOF STEP]
have *: "f i = nc" "nc = j"
[PROOF STATE]
proof (prove)
using this:
f i \<le> nc
\<not> j < nc
j \<le> f i

goal (1 subgoal):
 1. f i = nc &&& nc = j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f i = nc
nc = j

goal (1 subgoal):
 1. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
from i j
[PROOF STATE]
proof (chain)
picking this:
i < nr
\<not> j < nc
[PROOF STEP]
have p: "?p = []"
[PROOF STATE]
proof (prove)
using this:
i < nr
\<not> j < nc

goal (1 subgoal):
 1. local.pivot_positions_main i j = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.pivot_positions_main i j = []

goal (1 subgoal):
 1. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
from pivotB[of i "Suc 0"] *
[PROOF STATE]
proof (chain)
picking this:
i + Suc 0 < nr \<Longrightarrow> f (i + Suc 0) = nc \<or> Suc 0 + f i \<le> f (i + Suc 0)
f i = nc
nc = j
[PROOF STEP]
have "j \<le> f (Suc i) \<or> nr \<le> Suc i"
[PROOF STATE]
proof (prove)
using this:
i + Suc 0 < nr \<Longrightarrow> f (i + Suc 0) = nc \<or> Suc 0 + f i \<le> f (i + Suc 0)
f i = nc
nc = j

goal (1 subgoal):
 1. j \<le> f (Suc i) \<or> nr \<le> Suc i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<le> f (Suc i) \<or> nr \<le> Suc i

goal (1 subgoal):
 1. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
j \<le> f (Suc i) \<or> nr \<le> Suc i

goal (1 subgoal):
 1. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
fix i'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
assume **: "i \<le> i'" "i' < nr"
[PROOF STATE]
proof (state)
this:
i \<le> i'
i' < nr

goal (1 subgoal):
 1. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
hence "i + (i' - i) = i'"
[PROOF STATE]
proof (prove)
using this:
i \<le> i'
i' < nr

goal (1 subgoal):
 1. i + (i' - i) = i'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i + (i' - i) = i'

goal (1 subgoal):
 1. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
from pivotB[of i "i' - i", unfolded this] ** *
[PROOF STATE]
proof (chain)
picking this:
i' < nr \<Longrightarrow> f i' = nc \<or> i' - i + f i \<le> f i'
i \<le> i'
i' < nr
f i = nc
nc = j
[PROOF STEP]
have "nc \<le> f i'"
[PROOF STATE]
proof (prove)
using this:
i' < nr \<Longrightarrow> f i' = nc \<or> i' - i + f i \<le> f i'
i \<le> i'
i' < nr
f i = nc
nc = j

goal (1 subgoal):
 1. nc \<le> f i'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nc \<le> f i'

goal (1 subgoal):
 1. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
with pivot'(1)[OF \<open>i' < nr\<close>]
[PROOF STATE]
proof (chain)
picking this:
f i' \<le> nc
nc \<le> f i'
[PROOF STEP]
have "f i' = nc"
[PROOF STATE]
proof (prove)
using this:
f i' \<le> nc
nc \<le> f i'

goal (1 subgoal):
 1. f i' = nc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f i' = nc

goal (1 subgoal):
 1. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<le> ?i'2; ?i'2 < nr\<rbrakk> \<Longrightarrow> f ?i'2 = nc

goal (1 subgoal):
 1. \<not> j < nc \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<le> ?i'2; ?i'2 < nr\<rbrakk> \<Longrightarrow> f ?i'2 = nc

goal (1 subgoal):
 1. set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<le> ?i'2; ?i'2 < nr\<rbrakk> \<Longrightarrow> f ?i'2 = nc
\<lbrakk>j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j)))
\<lbrakk>j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j)))

goal (1 subgoal):
 1. set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
unfolding p id1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<le> ?i'2; ?i'2 < nr\<rbrakk> \<Longrightarrow> f ?i'2 = nc
\<lbrakk>j < nc; A $$ (i, j) = (0::'a); Suc j \<le> f i \<or> nr \<le> i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main i (Suc j)) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i (Suc j))) \<and> distinct (map fst (local.pivot_positions_main i (Suc j)))
\<lbrakk>j < nc; A $$ (i, j) \<noteq> (0::'a); Suc j \<le> f (Suc i) \<or> nr \<le> Suc i\<rbrakk> \<Longrightarrow> set (local.pivot_positions_main (Suc i) (Suc j)) = {(i', f i') |i'. Suc i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main (Suc i) (Suc j))) \<and> distinct (map fst (local.pivot_positions_main (Suc i) (Suc j)))

goal (1 subgoal):
 1. set [] = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd []) \<and> distinct (map fst [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))

goal (1 subgoal):
 1. \<not> i < nr \<Longrightarrow> set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
set (local.pivot_positions_main i j) = {(i', f i') |i'. i \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (local.pivot_positions_main i j)) \<and> distinct (map fst (local.pivot_positions_main i j))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pivot_fun_zero_row_iff: assumes pivot: "pivot_fun (A :: 'a :: semiring_1 mat) f nc"
  and A: "A \<in> carrier_mat nr nc"
  and i: "i < nr"
  shows "f i = nc \<longleftrightarrow> row A i = 0\<^sub>v nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat nr nc
[PROOF STEP]
have dim: "dim_row A = nr"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. dim_row A = nr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A = nr

goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
note pivot = pivot_funD[OF dim pivot i]
[PROOF STATE]
proof (state)
this:
f i \<le> nc
?j < f i \<Longrightarrow> A $$ (i, ?j) = (0::'a)
Suc i < nr \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc
f i < nc \<Longrightarrow> A $$ (i, f i) = (1::'a)
\<lbrakk>f i < nc; ?i' < nr; ?i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (?i', f i) = (0::'a)

goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
f i \<le> nc
?j < f i \<Longrightarrow> A $$ (i, ?j) = (0::'a)
Suc i < nr \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc
f i < nc \<Longrightarrow> A $$ (i, f i) = (1::'a)
\<lbrakk>f i < nc; ?i' < nr; ?i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (?i', f i) = (0::'a)

goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
assume "f i = nc"
[PROOF STATE]
proof (state)
this:
f i = nc

goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
from pivot(2)[unfolded this]
[PROOF STATE]
proof (chain)
picking this:
?j < nc \<Longrightarrow> A $$ (i, ?j) = (0::'a)
[PROOF STEP]
have "row A i = 0\<^sub>v nc"
[PROOF STATE]
proof (prove)
using this:
?j < nc \<Longrightarrow> A $$ (i, ?j) = (0::'a)

goal (1 subgoal):
 1. row A i = 0\<^sub>v nc
[PROOF STEP]
by (intro eq_vecI, insert A, auto simp: row_def)
[PROOF STATE]
proof (state)
this:
row A i = 0\<^sub>v nc

goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
f i = nc \<Longrightarrow> row A i = 0\<^sub>v nc

goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f i = nc \<Longrightarrow> row A i = 0\<^sub>v nc

goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
f i = nc \<Longrightarrow> row A i = 0\<^sub>v nc

goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
assume row: "row A i = 0\<^sub>v nc"
[PROOF STATE]
proof (state)
this:
row A i = 0\<^sub>v nc

goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
assume "f i \<noteq> nc"
[PROOF STATE]
proof (state)
this:
f i \<noteq> nc

goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
with pivot(1)
[PROOF STATE]
proof (chain)
picking this:
f i \<le> nc
f i \<noteq> nc
[PROOF STEP]
have "f i < nc"
[PROOF STATE]
proof (prove)
using this:
f i \<le> nc
f i \<noteq> nc

goal (1 subgoal):
 1. f i < nc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f i < nc

goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
with pivot(4)[OF this] i A arg_cong[OF row, of "\<lambda> v. v $ f i"]
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, f i) = (1::'a)
i < nr
A \<in> carrier_mat nr nc
row A i $ f i = 0\<^sub>v nc $ f i
f i < nc
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
A $$ (i, f i) = (1::'a)
i < nr
A \<in> carrier_mat nr nc
row A i $ f i = 0\<^sub>v nc $ f i
f i < nc

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

goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>row A i = 0\<^sub>v nc; f i \<noteq> nc\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f i = nc \<Longrightarrow> row A i = 0\<^sub>v nc
\<lbrakk>row A i = 0\<^sub>v nc; f i \<noteq> nc\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f i = nc \<Longrightarrow> row A i = 0\<^sub>v nc
\<lbrakk>row A i = 0\<^sub>v nc; f i \<noteq> nc\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (f i = nc) = (row A i = 0\<^sub>v nc)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f i = nc) = (row A i = 0\<^sub>v nc)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pivot_positions: assumes A: "A \<in> carrier_mat nr nc"
  and pivot: "pivot_fun A f nc"
  shows
    "set (pivot_positions A) = {(i, f i) | i. i < nr \<and> f i \<noteq> nc}"
    "distinct (map fst (pivot_positions A))"
    "distinct (map snd (pivot_positions A))"
    "length (pivot_positions A) = card { i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set (pivot_positions A) = {(i, f i) |i. i < nr \<and> f i \<noteq> nc} &&& distinct (map fst (pivot_positions A))) &&& distinct (map snd (pivot_positions A)) &&& length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. set (pivot_positions A) = {(i, f i) |i. i < nr \<and> f i \<noteq> nc}
 2. distinct (map fst (pivot_positions A))
 3. distinct (map snd (pivot_positions A))
 4. length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat nr nc
[PROOF STEP]
have dim: "dim_row A = nr"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. dim_row A = nr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A = nr

goal (4 subgoals):
 1. set (pivot_positions A) = {(i, f i) |i. i < nr \<and> f i \<noteq> nc}
 2. distinct (map fst (pivot_positions A))
 3. distinct (map snd (pivot_positions A))
 4. length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
let ?pp = "pivot_positions A"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. set (pivot_positions A) = {(i, f i) |i. i < nr \<and> f i \<noteq> nc}
 2. distinct (map fst (pivot_positions A))
 3. distinct (map snd (pivot_positions A))
 4. length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
show id: "set ?pp = {(i, f i) | i. i < nr \<and> f i \<noteq> nc}"
    and dist: "distinct (map fst ?pp)"
    and "distinct (map snd ?pp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (pivot_positions A) = {(i, f i) |i. i < nr \<and> f i \<noteq> nc} &&& distinct (map fst (pivot_positions A)) &&& distinct (map snd (pivot_positions A))
[PROOF STEP]
using pivot_positions_main[OF A pivot, of 0 0] A
[PROOF STATE]
proof (prove)
using this:
0 \<le> f 0 \<or> nr \<le> 0 \<Longrightarrow> set (pivot_positions_main A nr nc 0 0) = {(i', f i') |i'. 0 \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (pivot_positions_main A nr nc 0 0)) \<and> distinct (map fst (pivot_positions_main A nr nc 0 0))
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. set (pivot_positions A) = {(i, f i) |i. i < nr \<and> f i \<noteq> nc} &&& distinct (map fst (pivot_positions A)) &&& distinct (map snd (pivot_positions A))
[PROOF STEP]
unfolding pivot_positions_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> f 0 \<or> nr \<le> 0 \<Longrightarrow> set (pivot_positions_main A nr nc 0 0) = {(i', f i') |i'. 0 \<le> i' \<and> i' < nr} - UNIV \<times> {nc} \<and> distinct (map snd (pivot_positions_main A nr nc 0 0)) \<and> distinct (map fst (pivot_positions_main A nr nc 0 0))
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. set (pivot_positions_main A (dim_row A) (dim_col A) 0 0) = {(i, f i) |i. i < nr \<and> f i \<noteq> nc} &&& distinct (map fst (pivot_positions_main A (dim_row A) (dim_col A) 0 0)) &&& distinct (map snd (pivot_positions_main A (dim_row A) (dim_col A) 0 0))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (pivot_positions A) = {(i, f i) |i. i < nr \<and> f i \<noteq> nc}
distinct (map fst (pivot_positions A))
distinct (map snd (pivot_positions A))

goal (1 subgoal):
 1. length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
have "length ?pp = length (map fst ?pp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (pivot_positions A) = length (map fst (pivot_positions A))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (pivot_positions A) = length (map fst (pivot_positions A))

goal (1 subgoal):
 1. length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (pivot_positions A) = length (map fst (pivot_positions A))

goal (1 subgoal):
 1. length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
have "\<dots> = card (fst ` set ?pp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map fst (pivot_positions A)) = card (fst ` set (pivot_positions A))
[PROOF STEP]
using distinct_card[OF dist]
[PROOF STATE]
proof (prove)
using this:
card (set (map fst (pivot_positions A))) = length (map fst (pivot_positions A))

goal (1 subgoal):
 1. length (map fst (pivot_positions A)) = card (fst ` set (pivot_positions A))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (map fst (pivot_positions A)) = card (fst ` set (pivot_positions A))

goal (1 subgoal):
 1. length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (map fst (pivot_positions A)) = card (fst ` set (pivot_positions A))

goal (1 subgoal):
 1. length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
have "fst ` set ?pp = { i. i < nr \<and> f i \<noteq> nc}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` set (pivot_positions A) = {i. i < nr \<and> f i \<noteq> nc}
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` {(i, f i) |i. i < nr \<and> f i \<noteq> nc} = {i. i < nr \<and> f i \<noteq> nc}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst ` set (pivot_positions A) = {i. i < nr \<and> f i \<noteq> nc}

goal (1 subgoal):
 1. length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fst ` set (pivot_positions A) = {i. i < nr \<and> f i \<noteq> nc}

goal (1 subgoal):
 1. length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
have "\<dots> = { i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. i < nr \<and> f i \<noteq> nc} = {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
using pivot_fun_zero_row_iff[OF pivot A]
[PROOF STATE]
proof (prove)
using this:
?i < nr \<Longrightarrow> (f ?i = nc) = (row A ?i = 0\<^sub>v nc)

goal (1 subgoal):
 1. {i. i < nr \<and> f i \<noteq> nc} = {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. i < nr \<and> f i \<noteq> nc} = {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}

goal (1 subgoal):
 1. length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
show "length ?pp = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}"
[PROOF STATE]
proof (prove)
using this:
length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}

goal (1 subgoal):
 1. length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
length (pivot_positions A) = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}

goal:
No subgoals!
[PROOF STEP]
qed