[STATEMENT]
lemma inner_pres2:
assumes R: "\<forall>b<n. \<forall>a1<n. \<forall>a2<n. R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2 \<longleftrightarrow> P\<^sub>b ! b \<turnstile> a1 < a2" and
  inv: "invar2 A B M ai a" and m: "M ! b" and v: "var0 A {<n} = v"
  and after: "A1 = A[a' := A ! a' + 1]" "A2 = A[a := A ! a + 1]"
    "a' = B!b" "r = R\<^sub>b ! match A a'" "b = match A a"
shows "(r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b:=a]) M ai a' \<and> var0 A1 {<n} < v) \<and>
  (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)
[PROOF STEP]
let ?M = "{<ai+1} - {a}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)
[PROOF STEP]
note [simp] = after
[PROOF STATE]
proof (state)
this:
A1 = A[a' := A ! a' + 1]
A2 = A[a := A ! a + 1]
a' = B ! b
r = R\<^sub>b ! match A a'
b = match A a

goal (1 subgoal):
 1. (r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)
[PROOF STEP]
note inv' = inv[unfolded invar2_def]
[PROOF STATE]
proof (state)
this:
invAM A ({<ai + 1} - {a}) \<and> (invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n

goal (1 subgoal):
 1. (r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)
[PROOF STEP]
have A: "wf A" and M: "?M \<subseteq> {<n}" and invAM: "invAM A ?M" and invAB: "invAB A (\<alpha> B M) ?M"
    and mat: "matching A ?M" and pref_match: "pref_match A ?M"
    and as: "a \<le> ai \<and> ai < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.wf A &&& {<ai + 1} - {a} \<subseteq> {<n} &&& invAM A ({<ai + 1} - {a})) &&& (invAB A (\<alpha> B M) ({<ai + 1} - {a}) &&& matching A ({<ai + 1} - {a})) &&& pref_match A ({<ai + 1} - {a}) &&& a \<le> ai \<and> ai < n
[PROOF STEP]
using inv'
[PROOF STATE]
proof (prove)
using this:
invAM A ({<ai + 1} - {a}) \<and> (invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n) \<and> a \<le> ai \<and> ai < n

goal (1 subgoal):
 1. (local.wf A &&& {<ai + 1} - {a} \<subseteq> {<n} &&& invAM A ({<ai + 1} - {a})) &&& (invAB A (\<alpha> B M) ({<ai + 1} - {a}) &&& matching A ({<ai + 1} - {a})) &&& pref_match A ({<ai + 1} - {a}) &&& a \<le> ai \<and> ai < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.wf A
{<ai + 1} - {a} \<subseteq> {<n}
invAM A ({<ai + 1} - {a})
invAB A (\<alpha> B M) ({<ai + 1} - {a})
matching A ({<ai + 1} - {a})
pref_match A ({<ai + 1} - {a})
a \<le> ai \<and> ai < n

goal (1 subgoal):
 1. (r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)
[PROOF STEP]
note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]]
[PROOF STATE]
proof (state)
this:
pref_match' A ({<ai + 1} - {a})

goal (1 subgoal):
 1. (r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)
[PROOF STEP]
hence pref_match1: "\<forall>a<n. preferred A a \<subseteq> match A ` ?M"
[PROOF STATE]
proof (prove)
using this:
pref_match' A ({<ai + 1} - {a})

goal (1 subgoal):
 1. \<forall>aa<n. preferred A aa \<subseteq> match A ` ({<ai + 1} - {a})
[PROOF STEP]
unfolding pref_match'_def
[PROOF STATE]
proof (prove)
using this:
\<forall>aa<n. \<forall>b\<in>preferred A aa. \<exists>a'\<in>{<ai + 1} - {a}. b = match A a' \<and> P\<^sub>b ! b \<turnstile> a' < aa

goal (1 subgoal):
 1. \<forall>aa<n. preferred A aa \<subseteq> match A ` ({<ai + 1} - {a})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>aa<n. preferred A aa \<subseteq> match A ` ({<ai + 1} - {a})

goal (1 subgoal):
 1. (r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)
[PROOF STEP]
let ?a = "B ! match A a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)
[PROOF STEP]
have a: "a < n \<and> a \<notin> ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < n \<and> a \<notin> {<ai + 1} - {a}
[PROOF STEP]
using inv
[PROOF STATE]
proof (prove)
using this:
invar2 A B M ai a

goal (1 subgoal):
 1. a < n \<and> a \<notin> {<ai + 1} - {a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a < n \<and> a \<notin> {<ai + 1} - {a}

goal (1 subgoal):
 1. (r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)
[PROOF STEP]
have a': "?a \<in> ?M \<and> match A ?a = match A a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
[PROOF STEP]
using invAB match_less_n[OF A] a m inv
[PROOF STATE]
proof (prove)
using this:
invAB A (\<alpha> B M) ({<ai + 1} - {a})
?a < n \<Longrightarrow> match A ?a < n
a < n \<and> a \<notin> {<ai + 1} - {a}
M ! b
invar2 A B M ai a

goal (1 subgoal):
 1. B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
[PROOF STEP]
by (metis \<alpha>_Some ranI \<open>b = _\<close>)
[PROOF STATE]
proof (state)
this:
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a

goal (1 subgoal):
 1. (r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)
[PROOF STEP]
have "?M \<noteq> {<n}" and "?a < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<ai + 1} - {a} \<noteq> {<n} &&& B ! match A a < n
[PROOF STEP]
using M a a' atLeast0LessThan
[PROOF STATE]
proof (prove)
using this:
{<ai + 1} - {a} \<subseteq> {<n}
a < n \<and> a \<notin> {<ai + 1} - {a}
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
{<?n} = {..<?n}

goal (1 subgoal):
 1. {<ai + 1} - {a} \<noteq> {<n} &&& B ! match A a < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{<ai + 1} - {a} \<noteq> {<n}
B ! match A a < n

goal (1 subgoal):
 1. (r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)
[PROOF STEP]
have card: "card {<ai} = card ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {<ai} = card ({<ai + 1} - {a})
[PROOF STEP]
using as
[PROOF STATE]
proof (prove)
using this:
a \<le> ai \<and> ai < n

goal (1 subgoal):
 1. card {<ai} = card ({<ai + 1} - {a})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {<ai} = card ({<ai + 1} - {a})

goal (1 subgoal):
 1. (r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)
[PROOF STEP]
proof ((rule;rule;rule), goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. r ! a < r ! a' \<Longrightarrow> invar2 A1 (B[b := a]) M ai a'
 2. r ! a < r ! a' \<Longrightarrow> var0 A1 {<n} < v
 3. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 4. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
have *: "{<ai + 1} - {a} - {?a} \<union> {a} = {<ai + 1} - {?a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<ai + 1} - {a} - {B ! match A a} \<union> {a} = {<ai + 1} - {B ! match A a}
[PROOF STEP]
using inv a'
[PROOF STATE]
proof (prove)
using this:
invar2 A B M ai a
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a

goal (1 subgoal):
 1. {<ai + 1} - {a} - {B ! match A a} \<union> {a} = {<ai + 1} - {B ! match A a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{<ai + 1} - {a} - {B ! match A a} \<union> {a} = {<ai + 1} - {B ! match A a}

goal (4 subgoals):
 1. r ! a < r ! a' \<Longrightarrow> invar2 A1 (B[b := a]) M ai a'
 2. r ! a < r ! a' \<Longrightarrow> var0 A1 {<n} < v
 3. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 4. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
r ! a < r ! a'

goal (4 subgoals):
 1. r ! a < r ! a' \<Longrightarrow> invar2 A1 (B[b := a]) M ai a'
 2. r ! a < r ! a' \<Longrightarrow> var0 A1 {<n} < v
 3. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 4. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
hence unstab: "P\<^sub>b ! match A a' \<turnstile> a < a'"
[PROOF STATE]
proof (prove)
using this:
r ! a < r ! a'

goal (1 subgoal):
 1. P\<^sub>b ! match A a' \<turnstile> a < a'
[PROOF STEP]
using R a a' as P\<^sub>b_set P\<^sub>a_set match_less_n[OF A] n_def length_P\<^sub>b R
[PROOF STATE]
proof (prove)
using this:
r ! a < r ! a'
\<forall>b<n. \<forall>a1<n. \<forall>a2<n. (R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2) = (P\<^sub>b ! b \<turnstile> a1 < a2)
a < n \<and> a \<notin> {<ai + 1} - {a}
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
a \<le> ai \<and> ai < n
?b < n \<Longrightarrow> length (P\<^sub>b ! ?b) = n \<and> set (P\<^sub>b ! ?b) = {<n}
?a < n \<Longrightarrow> length (P\<^sub>a ! ?a) = n \<and> set (P\<^sub>a ! ?a) = {<n}
?a < n \<Longrightarrow> match A ?a < n
n \<equiv> length P\<^sub>a
length P\<^sub>b = n
\<forall>b<n. \<forall>a1<n. \<forall>a2<n. (R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2) = (P\<^sub>b ! b \<turnstile> a1 < a2)

goal (1 subgoal):
 1. P\<^sub>b ! match A a' \<turnstile> a < a'
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
P\<^sub>b ! match A a' \<turnstile> a < a'

goal (4 subgoals):
 1. r ! a < r ! a' \<Longrightarrow> invar2 A1 (B[b := a]) M ai a'
 2. r ! a < r ! a' \<Longrightarrow> var0 A1 {<n} < v
 3. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 4. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
have inj_dom: "inj_on (\<alpha> B M) (dom (\<alpha> B M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<alpha> B M) (dom (\<alpha> B M))
[PROOF STEP]
by (metis (mono_tags) domD inj_onI invAB)
[PROOF STATE]
proof (state)
this:
inj_on (\<alpha> B M) (dom (\<alpha> B M))

goal (4 subgoals):
 1. r ! a < r ! a' \<Longrightarrow> invar2 A1 (B[b := a]) M ai a'
 2. r ! a < r ! a' \<Longrightarrow> var0 A1 {<n} < v
 3. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 4. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
have invAB': "invAB A1 (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {?a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAB A1 (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})
[PROOF STEP]
using invAB_swap[OF invAB a a' inj_dom] * match_less_n[OF A] a m
[PROOF STATE]
proof (prove)
using this:
\<alpha> B M (match A a) = Some (B ! match A a) \<Longrightarrow> invAB (A[B ! match A a := A ! (B ! match A a) + 1]) (\<alpha> B M(match A a \<mapsto> a)) ({<ai + 1} - {a} - {B ! match A a} \<union> {a})
{<ai + 1} - {a} - {B ! match A a} \<union> {a} = {<ai + 1} - {B ! match A a}
?a < n \<Longrightarrow> match A ?a < n
a < n \<and> a \<notin> {<ai + 1} - {a}
M ! b

goal (1 subgoal):
 1. invAB A1 (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})
[PROOF STEP]
by (simp add: \<alpha>update2 inv')
[PROOF STATE]
proof (state)
this:
invAB A1 (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})

goal (4 subgoals):
 1. r ! a < r ! a' \<Longrightarrow> invar2 A1 (B[b := a]) M ai a'
 2. r ! a < r ! a' \<Longrightarrow> var0 A1 {<n} < v
 3. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 4. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar2 A1 (B[b := a]) M ai a'
[PROOF STEP]
using invAM_swap[OF invAM a a'] unstab invAB' inv a'
[PROOF STATE]
proof (prove)
using this:
P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {a} - {B ! match A a} \<union> {a})
P\<^sub>b ! match A a' \<turnstile> a < a'
invAB A1 (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})
invar2 A B M ai a
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a

goal (1 subgoal):
 1. invar2 A1 (B[b := a]) M ai a'
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {B ! match A a})
P\<^sub>b ! match A a' \<turnstile> a < a'
invAB A1 (\<alpha> (B[match A a := a]) M) ({<ai + 1} - {B ! match A a})
invar2 A B M ai a
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a

goal (1 subgoal):
 1. invar2 A1 (B[b := a]) M ai a'
[PROOF STEP]
by (simp add: insert_absorb \<alpha>update2)
[PROOF STATE]
proof (state)
this:
invar2 A1 (B[b := a]) M ai a'

goal (3 subgoals):
 1. r ! a < r ! a' \<Longrightarrow> var0 A1 {<n} < v
 2. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 3. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. r ! a < r ! a' \<Longrightarrow> var0 A1 {<n} < v
 2. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 3. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
r ! a < r ! a'

goal (3 subgoals):
 1. r ! a < r ! a' \<Longrightarrow> var0 A1 {<n} < v
 2. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 3. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
hence unstab: "P\<^sub>b ! match A a' \<turnstile> a < a'"
[PROOF STATE]
proof (prove)
using this:
r ! a < r ! a'

goal (1 subgoal):
 1. P\<^sub>b ! match A a' \<turnstile> a < a'
[PROOF STEP]
using R a a' as P\<^sub>b_set P\<^sub>a_set match_less_n[OF A] n_def length_P\<^sub>b R
[PROOF STATE]
proof (prove)
using this:
r ! a < r ! a'
\<forall>b<n. \<forall>a1<n. \<forall>a2<n. (R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2) = (P\<^sub>b ! b \<turnstile> a1 < a2)
a < n \<and> a \<notin> {<ai + 1} - {a}
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
a \<le> ai \<and> ai < n
?b < n \<Longrightarrow> length (P\<^sub>b ! ?b) = n \<and> set (P\<^sub>b ! ?b) = {<n}
?a < n \<Longrightarrow> length (P\<^sub>a ! ?a) = n \<and> set (P\<^sub>a ! ?a) = {<n}
?a < n \<Longrightarrow> match A ?a < n
n \<equiv> length P\<^sub>a
length P\<^sub>b = n
\<forall>b<n. \<forall>a1<n. \<forall>a2<n. (R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2) = (P\<^sub>b ! b \<turnstile> a1 < a2)

goal (1 subgoal):
 1. P\<^sub>b ! match A a' \<turnstile> a < a'
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
P\<^sub>b ! match A a' \<turnstile> a < a'

goal (3 subgoals):
 1. r ! a < r ! a' \<Longrightarrow> var0 A1 {<n} < v
 2. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 3. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
from invAM_swap[OF invAM a a'] unstab
[PROOF STATE]
proof (chain)
picking this:
P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {a} - {B ! match A a} \<union> {a})
P\<^sub>b ! match A a' \<turnstile> a < a'
[PROOF STEP]
have wf: "wf (A[a' := A ! a' + 1])"
[PROOF STATE]
proof (prove)
using this:
P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {a} - {B ! match A a} \<union> {a})
P\<^sub>b ! match A a' \<turnstile> a < a'

goal (1 subgoal):
 1. local.wf (A[a' := A ! a' + 1])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.wf (A[a' := A ! a' + 1])

goal (3 subgoals):
 1. r ! a < r ! a' \<Longrightarrow> var0 A1 {<n} < v
 2. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 3. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var0 A1 {<n} < v
[PROOF STEP]
using v var0_next2[OF wf]
[PROOF STATE]
proof (prove)
using this:
var0 A {<n} = v
a' < n \<Longrightarrow> var0 (A[a' := A ! a' + 1]) {<n} < var0 A {<n}

goal (1 subgoal):
 1. var0 A1 {<n} < v
[PROOF STEP]
using \<open>B ! match A a < n\<close> assms(5,7,9)
[PROOF STATE]
proof (prove)
using this:
var0 A {<n} = v
a' < n \<Longrightarrow> var0 (A[a' := A ! a' + 1]) {<n} < var0 A {<n}
B ! match A a < n
A1 = A[a' := A ! a' + 1]
a' = B ! b
b = match A a

goal (1 subgoal):
 1. var0 A1 {<n} < v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
var0 A1 {<n} < v

goal (2 subgoals):
 1. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 2. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 2. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
have *: "\<forall>b. b < n \<and> M!b \<longrightarrow> a \<noteq> B!b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b. b < n \<and> M ! b \<longrightarrow> a \<noteq> B ! b
[PROOF STEP]
by (metis invAB ranI \<alpha>_Some a)
[PROOF STATE]
proof (state)
this:
\<forall>b. b < n \<and> M ! b \<longrightarrow> a \<noteq> B ! b

goal (2 subgoals):
 1. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 2. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
\<not> r ! a < r ! a'

goal (2 subgoals):
 1. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 2. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
hence unstab: "\<not> P\<^sub>b ! match A a' \<turnstile> a < a'"
[PROOF STATE]
proof (prove)
using this:
\<not> r ! a < r ! a'

goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A a' \<turnstile> a < a'
[PROOF STEP]
using R a a' as P\<^sub>b_set P\<^sub>a_set match_less_n[OF A] n_def length_P\<^sub>b
[PROOF STATE]
proof (prove)
using this:
\<not> r ! a < r ! a'
\<forall>b<n. \<forall>a1<n. \<forall>a2<n. (R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2) = (P\<^sub>b ! b \<turnstile> a1 < a2)
a < n \<and> a \<notin> {<ai + 1} - {a}
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
a \<le> ai \<and> ai < n
?b < n \<Longrightarrow> length (P\<^sub>b ! ?b) = n \<and> set (P\<^sub>b ! ?b) = {<n}
?a < n \<Longrightarrow> length (P\<^sub>a ! ?a) = n \<and> set (P\<^sub>a ! ?a) = {<n}
?a < n \<Longrightarrow> match A ?a < n
n \<equiv> length P\<^sub>a
length P\<^sub>b = n

goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A a' \<turnstile> a < a'
[PROOF STEP]
by (simp add: ranking_iff_pref)
[PROOF STATE]
proof (state)
this:
\<not> P\<^sub>b ! match A a' \<turnstile> a < a'

goal (2 subgoals):
 1. \<not> r ! a < r ! a' \<Longrightarrow> invar2 A2 B M ai a
 2. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> P\<^sub>b ! match A a' \<turnstile> a < a'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<not> P\<^sub>b ! match A a' \<turnstile> a < a'

goal (1 subgoal):
 1. invar2 A2 B M ai a
[PROOF STEP]
using invAM_next[OF invAM a a'] 3 inv *
[PROOF STATE]
proof (prove)
using this:
\<not> P\<^sub>b ! match A a' \<turnstile> a < a'
\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invAM (A[a := A ! a + 1]) ({<ai + 1} - {a})
\<not> r ! a < r ! a'
invar2 A B M ai a
\<forall>b. b < n \<and> M ! b \<longrightarrow> a \<noteq> B ! b

goal (1 subgoal):
 1. invar2 A2 B M ai a
[PROOF STEP]
by (simp add: match_def)
[PROOF STATE]
proof (state)
this:
invar2 A2 B M ai a

goal (1 subgoal):
 1. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
\<not> r ! a < r ! a'

goal (1 subgoal):
 1. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
hence unstab: "\<not> P\<^sub>b ! match A a' \<turnstile> a < a'"
[PROOF STATE]
proof (prove)
using this:
\<not> r ! a < r ! a'

goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A a' \<turnstile> a < a'
[PROOF STEP]
using R a a' as P\<^sub>b_set P\<^sub>a_set match_less_n[OF A] n_def length_P\<^sub>b
[PROOF STATE]
proof (prove)
using this:
\<not> r ! a < r ! a'
\<forall>b<n. \<forall>a1<n. \<forall>a2<n. (R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2) = (P\<^sub>b ! b \<turnstile> a1 < a2)
a < n \<and> a \<notin> {<ai + 1} - {a}
B ! match A a \<in> {<ai + 1} - {a} \<and> match A (B ! match A a) = match A a
a \<le> ai \<and> ai < n
?b < n \<Longrightarrow> length (P\<^sub>b ! ?b) = n \<and> set (P\<^sub>b ! ?b) = {<n}
?a < n \<Longrightarrow> length (P\<^sub>a ! ?a) = n \<and> set (P\<^sub>a ! ?a) = {<n}
?a < n \<Longrightarrow> match A ?a < n
n \<equiv> length P\<^sub>a
length P\<^sub>b = n

goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A a' \<turnstile> a < a'
[PROOF STEP]
by (simp add: ranking_iff_pref)
[PROOF STATE]
proof (state)
this:
\<not> P\<^sub>b ! match A a' \<turnstile> a < a'

goal (1 subgoal):
 1. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
from invAM_next[OF invAM a a'] unstab
[PROOF STATE]
proof (chain)
picking this:
\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invAM (A[a := A ! a + 1]) ({<ai + 1} - {a})
\<not> P\<^sub>b ! match A a' \<turnstile> a < a'
[PROOF STEP]
have wf: "wf (A[a := A ! a + 1])"
[PROOF STATE]
proof (prove)
using this:
\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> invAM (A[a := A ! a + 1]) ({<ai + 1} - {a})
\<not> P\<^sub>b ! match A a' \<turnstile> a < a'

goal (1 subgoal):
 1. local.wf (A[a := A ! a + 1])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.wf (A[a := A ! a + 1])

goal (1 subgoal):
 1. \<not> r ! a < r ! a' \<Longrightarrow> var0 A2 {<n} < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var0 A2 {<n} < v
[PROOF STEP]
using v var0_next2[OF wf] a
[PROOF STATE]
proof (prove)
using this:
var0 A {<n} = v
a < n \<Longrightarrow> var0 (A[a := A ! a + 1]) {<n} < var0 A {<n}
a < n \<and> a \<notin> {<ai + 1} - {a}

goal (1 subgoal):
 1. var0 A2 {<n} < v
[PROOF STEP]
using assms(6)
[PROOF STATE]
proof (prove)
using this:
var0 A {<n} = v
a < n \<Longrightarrow> var0 (A[a := A ! a + 1]) {<n} < var0 A {<n}
a < n \<and> a \<notin> {<ai + 1} - {a}
A2 = A[a := A ! a + 1]

goal (1 subgoal):
 1. var0 A2 {<n} < v
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
var0 A2 {<n} < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(r ! a < r ! a' \<longrightarrow> invar2 A1 (B[b := a]) M ai a' \<and> var0 A1 {<n} < v) \<and> (\<not> r ! a < r ! a' \<longrightarrow> invar2 A2 B M ai a \<and> var0 A2 {<n} < v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Gale_Shapley6':
assumes "R\<^sub>b = map ranking P\<^sub>b"
shows
"VARS A B M ai a a' b r
 [ai = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False]
 WHILE ai < n
 INV { invar1 A B M ai }
 VAR {z = n - ai}
 DO a := ai; b := match A a;
  WHILE M ! b
  INV { invar2 A B M ai a \<and> b = match A a \<and> z = n-ai }
  VAR {var0 A {<n}}
  DO a' := B ! b; r := R\<^sub>b ! match A a';
     IF r ! a < r ! a'
     THEN B[b] := a; A[a'] := A!a'+1; a := a'
     ELSE A[a] := A!a+1
     FI;
     b := match A a
  OD;
  B[b] := a; M[b] := True; ai := ai+1
 OD
 [matching A {<n} \<and> stable A {<n} \<and> opti\<^sub>a A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [ai = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False]
WHILE ai < n INV {invar1 A B M ai}  VAR {z = n - ai}
DO a := ai; b := match A a; WHILE M ! b INV {invar2 A B M ai a \<and> b = match A a \<and> z = n - ai}  VAR {var0 A {<n}}
DO a' := B ! b; r := R\<^sub>b ! match A a'; IF r ! a < r ! a' THEN B := B[b := a]; A := A[a' := A ! a' + 1]; a := a'  ELSE A := A[a := A ! a + 1] FI; b := match A a OD; B := B[b := a]; M := M[b := True]; ai := ai + 1 OD
[matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A]
[PROOF STEP]
proof (vcg_tc, goal_cases)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>A B M ai a a' b r. ai = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False \<Longrightarrow> invar1 A B M ai
 2. \<And>z A B M ai a a' b r. (invar1 A B M ai \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invar2 A B M ai ai \<and> match A ai = match A ai \<and> z = n - ai
 3. \<And>z na A B M ai a a' b r. ((invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> M ! b) \<and> var0 A {<n} = na \<Longrightarrow> (R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[B ! b := A ! (B ! b) + 1], B[b := a], M, ai, B ! b, B ! b, match (A[B ! b := A ! (B ! b) + 1]) (B ! b), R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! b, match (A[a := A ! a + 1]) a, R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na))
 4. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 5. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
ai_ = 0 \<and> A_ = replicate n 0 \<and> length B_ = n \<and> M_ = replicate n False

goal (5 subgoals):
 1. \<And>A B M ai a a' b r. ai = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False \<Longrightarrow> invar1 A B M ai
 2. \<And>z A B M ai a a' b r. (invar1 A B M ai \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invar2 A B M ai ai \<and> match A ai = match A ai \<and> z = n - ai
 3. \<And>z na A B M ai a a' b r. ((invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> M ! b) \<and> var0 A {<n} = na \<Longrightarrow> (R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[B ! b := A ! (B ! b) + 1], B[b := a], M, ai, B ! b, B ! b, match (A[B ! b := A ! (B ! b) + 1]) (B ! b), R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! b, match (A[a := A ! a + 1]) a, R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na))
 4. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 5. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ai_ = 0 \<and> A_ = replicate n 0 \<and> length B_ = n \<and> M_ = replicate n False

goal (1 subgoal):
 1. invar1 A_ B_ M_ ai_
[PROOF STEP]
(* outer invar holds initially *)
[PROOF STATE]
proof (prove)
using this:
ai_ = 0 \<and> A_ = replicate n 0 \<and> length B_ = n \<and> M_ = replicate n False

goal (1 subgoal):
 1. invar1 A_ B_ M_ ai_
[PROOF STEP]
by(auto simp: stable_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def opti\<^sub>a_def \<alpha>_def cong: conj_cong)
[PROOF STATE]
proof (state)
this:
invar1 A_ B_ M_ ai_

goal (4 subgoals):
 1. \<And>z A B M ai a a' b r. (invar1 A B M ai \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invar2 A B M ai ai \<and> match A ai = match A ai \<and> z = n - ai
 2. \<And>z na A B M ai a a' b r. ((invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> M ! b) \<and> var0 A {<n} = na \<Longrightarrow> (R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[B ! b := A ! (B ! b) + 1], B[b := a], M, ai, B ! b, B ! b, match (A[B ! b := A ! (B ! b) + 1]) (B ! b), R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! b, match (A[a := A ! a + 1]) a, R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na))
 3. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 4. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>z A B M ai a a' b r. (invar1 A B M ai \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invar2 A B M ai ai \<and> match A ai = match A ai \<and> z = n - ai
 2. \<And>z na A B M ai a a' b r. ((invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> M ! b) \<and> var0 A {<n} = na \<Longrightarrow> (R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[B ! b := A ! (B ! b) + 1], B[b := a], M, ai, B ! b, B ! b, match (A[B ! b := A ! (B ! b) + 1]) (B ! b), R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! b, match (A[a := A ! a + 1]) a, R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na))
 3. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 4. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
(invar1 A_ B_ M_ ai_ \<and> ai_ < n) \<and> n - ai_ = z_

goal (4 subgoals):
 1. \<And>z A B M ai a a' b r. (invar1 A B M ai \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invar2 A B M ai ai \<and> match A ai = match A ai \<and> z = n - ai
 2. \<And>z na A B M ai a a' b r. ((invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> M ! b) \<and> var0 A {<n} = na \<Longrightarrow> (R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[B ! b := A ! (B ! b) + 1], B[b := a], M, ai, B ! b, B ! b, match (A[B ! b := A ! (B ! b) + 1]) (B ! b), R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! b, match (A[a := A ! a + 1]) a, R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na))
 3. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 4. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
(* outer invar and b ibplies inner invar *)
[PROOF STATE]
proof (state)
this:
(invar1 A_ B_ M_ ai_ \<and> ai_ < n) \<and> n - ai_ = z_

goal (4 subgoals):
 1. \<And>z A B M ai a a' b r. (invar1 A B M ai \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invar2 A B M ai ai \<and> match A ai = match A ai \<and> z = n - ai
 2. \<And>z na A B M ai a a' b r. ((invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> M ! b) \<and> var0 A {<n} = na \<Longrightarrow> (R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[B ! b := A ! (B ! b) + 1], B[b := a], M, ai, B ! b, B ! b, match (A[B ! b := A ! (B ! b) + 1]) (B ! b), R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! b, match (A[a := A ! a + 1]) a, R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na))
 3. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 4. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(invar1 A_ B_ M_ ai_ \<and> ai_ < n) \<and> n - ai_ = z_

goal (1 subgoal):
 1. invar2 A_ B_ M_ ai_ ai_ \<and> match A_ ai_ = match A_ ai_ \<and> z_ = n - ai_
[PROOF STEP]
by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
[PROOF STATE]
proof (state)
this:
invar2 A_ B_ M_ ai_ ai_ \<and> match A_ ai_ = match A_ ai_ \<and> z_ = n - ai_

goal (3 subgoals):
 1. \<And>z na A B M ai a a' b r. ((invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> M ! b) \<and> var0 A {<n} = na \<Longrightarrow> (R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[B ! b := A ! (B ! b) + 1], B[b := a], M, ai, B ! b, B ! b, match (A[B ! b := A ! (B ! b) + 1]) (B ! b), R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! b, match (A[a := A ! a + 1]) a, R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na))
 2. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 3. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>z na A B M ai a a' b r. ((invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> M ! b) \<and> var0 A {<n} = na \<Longrightarrow> (R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[B ! b := A ! (B ! b) + 1], B[b := a], M, ai, B ! b, B ! b, match (A[B ! b := A ! (B ! b) + 1]) (B ! b), R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! b, match (A[a := A ! a + 1]) a, R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na))
 2. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 3. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
((invar2 A_ B_ M_ ai_ a_ \<and> b_ = match A_ a_ \<and> z_ = n - ai_) \<and> M_ ! b_) \<and> var0 A_ {<n} = n_

goal (3 subgoals):
 1. \<And>z na A B M ai a a' b r. ((invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> M ! b) \<and> var0 A {<n} = na \<Longrightarrow> (R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[B ! b := A ! (B ! b) + 1], B[b := a], M, ai, B ! b, B ! b, match (A[B ! b := A ! (B ! b) + 1]) (B ! b), R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! b, match (A[a := A ! a + 1]) a, R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na))
 2. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 3. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
(* preservation of inner invar *)
[PROOF STATE]
proof (state)
this:
((invar2 A_ B_ M_ ai_ a_ \<and> b_ = match A_ a_ \<and> z_ = n - ai_) \<and> M_ ! b_) \<and> var0 A_ {<n} = n_

goal (3 subgoals):
 1. \<And>z na A B M ai a a' b r. ((invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> M ! b) \<and> var0 A {<n} = na \<Longrightarrow> (R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[B ! b := A ! (B ! b) + 1], B[b := a], M, ai, B ! b, B ! b, match (A[B ! b := A ! (B ! b) + 1]) (B ! b), R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! b, match (A[a := A ! a + 1]) a, R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na))
 2. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 3. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
have R: "\<forall>b<n. \<forall>a1<n. \<forall>a2<n. R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2 \<longleftrightarrow> P\<^sub>b ! b \<turnstile> a1 < a2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b<n. \<forall>a1<n. \<forall>a2<n. (R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2) = (P\<^sub>b ! b \<turnstile> a1 < a2)
[PROOF STEP]
by (simp add: P\<^sub>b_set \<open>R\<^sub>b = _\<close> length_P\<^sub>b ranking_iff_pref)
[PROOF STATE]
proof (state)
this:
\<forall>b<n. \<forall>a1<n. \<forall>a2<n. (R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2) = (P\<^sub>b ! b \<turnstile> a1 < a2)

goal (3 subgoals):
 1. \<And>z na A B M ai a a' b r. ((invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> M ! b) \<and> var0 A {<n} = na \<Longrightarrow> (R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[B ! b := A ! (B ! b) + 1], B[b := a], M, ai, B ! b, B ! b, match (A[B ! b := A ! (B ! b) + 1]) (B ! b), R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! b) ! a < R\<^sub>b ! match A (B ! b) ! (B ! b) \<longrightarrow> (A[a := A ! a + 1], B, M, ai, a, B ! b, match (A[a := A ! a + 1]) a, R\<^sub>b ! match A (B ! b)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < na))
 2. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 3. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (R\<^sub>b ! match A_ (B_ ! b_) ! a_ < R\<^sub>b ! match A_ (B_ ! b_) ! (B_ ! b_) \<longrightarrow> (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1], B_[b_ := a_], M_, ai_, B_ ! b_, B_ ! b_, match (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_ ! b_), R\<^sub>b ! match A_ (B_ ! b_)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z_ = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < n_)) \<and> (\<not> R\<^sub>b ! match A_ (B_ ! b_) ! a_ < R\<^sub>b ! match A_ (B_ ! b_) ! (B_ ! b_) \<longrightarrow> (A_[a_ := A_ ! a_ + 1], B_, M_, ai_, a_, B_ ! b_, match (A_[a_ := A_ ! a_ + 1]) a_, R\<^sub>b ! match A_ (B_ ! b_)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z_ = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < n_))
[PROOF STEP]
proof (simp only: mem_Collect_eq prod.case, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (R\<^sub>b ! match A_ (B_ ! b_) ! a_ < R\<^sub>b ! match A_ (B_ ! b_) ! (B_ ! b_) \<longrightarrow> (invar2 (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_[b_ := a_]) M_ ai_ (B_ ! b_) \<and> match (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_ ! b_) = match (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_ ! b_) \<and> z_ = n - ai_) \<and> var0 (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) {<n} < n_) \<and> (\<not> R\<^sub>b ! match A_ (B_ ! b_) ! a_ < R\<^sub>b ! match A_ (B_ ! b_) ! (B_ ! b_) \<longrightarrow> (invar2 (A_[a_ := A_ ! a_ + 1]) B_ M_ ai_ a_ \<and> match (A_[a_ := A_ ! a_ + 1]) a_ = match (A_[a_ := A_ ! a_ + 1]) a_ \<and> z_ = n - ai_) \<and> var0 (A_[a_ := A_ ! a_ + 1]) {<n} < n_)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. (R\<^sub>b ! match A_ (B_ ! b_) ! a_ < R\<^sub>b ! match A_ (B_ ! b_) ! (B_ ! b_) \<longrightarrow> (invar2 (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_[b_ := a_]) M_ ai_ (B_ ! b_) \<and> match (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_ ! b_) = match (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_ ! b_) \<and> z_ = n - ai_) \<and> var0 (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) {<n} < n_) \<and> (\<not> R\<^sub>b ! match A_ (B_ ! b_) ! a_ < R\<^sub>b ! match A_ (B_ ! b_) ! (B_ ! b_) \<longrightarrow> (invar2 (A_[a_ := A_ ! a_ + 1]) B_ M_ ai_ a_ \<and> match (A_[a_ := A_ ! a_ + 1]) a_ = match (A_[a_ := A_ ! a_ + 1]) a_ \<and> z_ = n - ai_) \<and> var0 (A_[a_ := A_ ! a_ + 1]) {<n} < n_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (R\<^sub>b ! match A_ (B_ ! b_) ! a_ < R\<^sub>b ! match A_ (B_ ! b_) ! (B_ ! b_) \<longrightarrow> (invar2 (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_[b_ := a_]) M_ ai_ (B_ ! b_) \<and> match (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_ ! b_) = match (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_ ! b_) \<and> z_ = n - ai_) \<and> var0 (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) {<n} < n_) \<and> (\<not> R\<^sub>b ! match A_ (B_ ! b_) ! a_ < R\<^sub>b ! match A_ (B_ ! b_) ! (B_ ! b_) \<longrightarrow> (invar2 (A_[a_ := A_ ! a_ + 1]) B_ M_ ai_ a_ \<and> match (A_[a_ := A_ ! a_ + 1]) a_ = match (A_[a_ := A_ ! a_ + 1]) a_ \<and> z_ = n - ai_) \<and> var0 (A_[a_ := A_ ! a_ + 1]) {<n} < n_)
[PROOF STEP]
using inner_pres2[OF R _ _ refl refl refl] 3
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>invar2 ?A ?B ?M ?ai ?a; ?M ! ?b; ?a' = ?B ! ?b; ?r = R\<^sub>b ! match ?A ?a'; ?b = match ?A ?a\<rbrakk> \<Longrightarrow> (?r ! ?a < ?r ! ?a' \<longrightarrow> invar2 (?A[?a' := ?A ! ?a' + 1]) (?B[?b := ?a]) ?M ?ai ?a' \<and> var0 (?A[?a' := ?A ! ?a' + 1]) {<n} < var0 ?A {<n}) \<and> (\<not> ?r ! ?a < ?r ! ?a' \<longrightarrow> invar2 (?A[?a := ?A ! ?a + 1]) ?B ?M ?ai ?a \<and> var0 (?A[?a := ?A ! ?a + 1]) {<n} < var0 ?A {<n})
((invar2 A_ B_ M_ ai_ a_ \<and> b_ = match A_ a_ \<and> z_ = n - ai_) \<and> M_ ! b_) \<and> var0 A_ {<n} = n_

goal (1 subgoal):
 1. (R\<^sub>b ! match A_ (B_ ! b_) ! a_ < R\<^sub>b ! match A_ (B_ ! b_) ! (B_ ! b_) \<longrightarrow> (invar2 (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_[b_ := a_]) M_ ai_ (B_ ! b_) \<and> match (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_ ! b_) = match (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_ ! b_) \<and> z_ = n - ai_) \<and> var0 (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) {<n} < n_) \<and> (\<not> R\<^sub>b ! match A_ (B_ ! b_) ! a_ < R\<^sub>b ! match A_ (B_ ! b_) ! (B_ ! b_) \<longrightarrow> (invar2 (A_[a_ := A_ ! a_ + 1]) B_ M_ ai_ a_ \<and> match (A_[a_ := A_ ! a_ + 1]) a_ = match (A_[a_ := A_ ! a_ + 1]) a_ \<and> z_ = n - ai_) \<and> var0 (A_[a_ := A_ ! a_ + 1]) {<n} < n_)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(R\<^sub>b ! match A_ (B_ ! b_) ! a_ < R\<^sub>b ! match A_ (B_ ! b_) ! (B_ ! b_) \<longrightarrow> (invar2 (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_[b_ := a_]) M_ ai_ (B_ ! b_) \<and> match (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_ ! b_) = match (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_ ! b_) \<and> z_ = n - ai_) \<and> var0 (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) {<n} < n_) \<and> (\<not> R\<^sub>b ! match A_ (B_ ! b_) ! a_ < R\<^sub>b ! match A_ (B_ ! b_) ! (B_ ! b_) \<longrightarrow> (invar2 (A_[a_ := A_ ! a_ + 1]) B_ M_ ai_ a_ \<and> match (A_[a_ := A_ ! a_ + 1]) a_ = match (A_[a_ := A_ ! a_ + 1]) a_ \<and> z_ = n - ai_) \<and> var0 (A_[a_ := A_ ! a_ + 1]) {<n} < n_)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(R\<^sub>b ! match A_ (B_ ! b_) ! a_ < R\<^sub>b ! match A_ (B_ ! b_) ! (B_ ! b_) \<longrightarrow> (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1], B_[b_ := a_], M_, ai_, B_ ! b_, B_ ! b_, match (A_[B_ ! b_ := A_ ! (B_ ! b_) + 1]) (B_ ! b_), R\<^sub>b ! match A_ (B_ ! b_)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z_ = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < n_)) \<and> (\<not> R\<^sub>b ! match A_ (B_ ! b_) ! a_ < R\<^sub>b ! match A_ (B_ ! b_) ! (B_ ! b_) \<longrightarrow> (A_[a_ := A_ ! a_ + 1], B_, M_, ai_, a_, B_ ! b_, match (A_[a_ := A_ ! a_ + 1]) a_, R\<^sub>b ! match A_ (B_ ! b_)) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar2 A B M ai a \<and> b = match A a \<and> z_ = n - ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> var0 A {<n}) < n_))

goal (2 subgoals):
 1. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 2. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 2. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
(invar2 A_ B_ M_ ai_ a_ \<and> b_ = match A_ a_ \<and> z_ = n - ai_) \<and> \<not> M_ ! b_

goal (2 subgoals):
 1. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 2. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
(* inner invar' and not b ibplies outer invar *)
[PROOF STATE]
proof (state)
this:
(invar2 A_ B_ M_ ai_ a_ \<and> b_ = match A_ a_ \<and> z_ = n - ai_) \<and> \<not> M_ ! b_

goal (2 subgoals):
 1. \<And>z A B M ai a a' b r. (invar2 A B M ai a \<and> b = match A a \<and> z = n - ai) \<and> \<not> M ! b \<Longrightarrow> (A, B[b := a], M[b := True], ai + 1, a, a', b, r) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z)
 2. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A_, B_[b_ := a_], M_[b_ := True], ai_ + 1, a_, a'_, b_, r_) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z_)
[PROOF STEP]
proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. invar1 A_ (B_[b_ := a_]) (M_[b_ := True]) (ai_ + 1)
 2. n - (ai_ + 1) < z_
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invar1 A_ (B_[b_ := a_]) (M_[b_ := True]) (ai_ + 1)
 2. n - (ai_ + 1) < z_
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar1 A_ (B_[b_ := a_]) (M_[b_ := True]) (ai_ + 1)
[PROOF STEP]
using 4 inner_to_outer
[PROOF STATE]
proof (prove)
using this:
(invar2 A_ B_ M_ ai_ a_ \<and> b_ = match A_ a_ \<and> z_ = n - ai_) \<and> \<not> M_ ! b_
\<lbrakk>invar2 ?A ?B ?M ?ai ?a \<and> ?b = match ?A ?a; \<not> ?M ! ?b\<rbrakk> \<Longrightarrow> invar1 ?A (?B[?b := ?a]) (?M[?b := True]) (?ai + 1)

goal (1 subgoal):
 1. invar1 A_ (B_[b_ := a_]) (M_[b_ := True]) (ai_ + 1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
invar1 A_ (B_[b_ := a_]) (M_[b_ := True]) (ai_ + 1)

goal (1 subgoal):
 1. n - (ai_ + 1) < z_
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n - (ai_ + 1) < z_
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. n - (ai_ + 1) < z_
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n - (ai_ + 1) < z_
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
(invar2 A_ B_ M_ ai_ a_ \<and> b_ = match A_ a_ \<and> z_ = n - ai_) \<and> \<not> M_ ! b_

goal (1 subgoal):
 1. n - (ai_ + 1) < z_
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n - (ai_ + 1) < z_

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(A_, B_[b_ := a_], M_[b_ := True], ai_ + 1, a_, a'_, b_, r_) \<in> _Collect s ((case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> invar1 A B M ai) \<and> (case s of (A, B, M, ai, a, a', b, r) \<Rightarrow> n - ai) < z_)

goal (1 subgoal):
 1. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 5
[PROOF STATE]
proof (state)
this:
invar1 A_ B_ M_ ai_ \<and> \<not> ai_ < n

goal (1 subgoal):
 1. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
(* outer invar and not b ibplies post *)
[PROOF STATE]
proof (state)
this:
invar1 A_ B_ M_ ai_ \<and> \<not> ai_ < n

goal (1 subgoal):
 1. \<And>A B M ai a a' b r. invar1 A B M ai \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
invar1 A_ B_ M_ ai_ \<and> \<not> ai_ < n

goal (1 subgoal):
 1. matching A_ {<n} \<and> local.stable A_ {<n} \<and> opti\<^sub>a A_
[PROOF STEP]
using pref_match_stable
[PROOF STATE]
proof (prove)
using this:
invar1 A_ B_ M_ ai_ \<and> \<not> ai_ < n
\<lbrakk>matching ?A {<n}; pref_match ?A {<n}\<rbrakk> \<Longrightarrow> local.stable ?A {<n}

goal (1 subgoal):
 1. matching A_ {<n} \<and> local.stable A_ {<n} \<and> opti\<^sub>a A_
[PROOF STEP]
unfolding invAM_def invar1_def
[PROOF STATE]
proof (prove)
using this:
((matching A_ {<ai_} \<and> {<ai_} \<subseteq> {<n} \<and> pref_match A_ {<ai_} \<and> opti\<^sub>a A_) \<and> (invAB A_ (\<alpha> B_ M_) {<ai_} \<and> length B_ = n \<and> length M_ = n) \<and> ai_ \<le> n) \<and> \<not> ai_ < n
\<lbrakk>matching ?A {<n}; pref_match ?A {<n}\<rbrakk> \<Longrightarrow> local.stable ?A {<n}

goal (1 subgoal):
 1. matching A_ {<n} \<and> local.stable A_ {<n} \<and> opti\<^sub>a A_
[PROOF STEP]
by(metis le_neq_implies_less)
[PROOF STATE]
proof (state)
this:
matching A_ {<n} \<and> local.stable A_ {<n} \<and> opti\<^sub>a A_

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R_iff_P:
assumes "R\<^sub>b = map ranking P\<^sub>b" "invar2' A B M ai a" "ai < n" "M ! match A a"
shows "(R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) =
  (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
[PROOF STEP]
have R: "\<forall>b<n. \<forall>a1<n. \<forall>a2<n. R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2 \<longleftrightarrow> P\<^sub>b ! b \<turnstile> a1 < a2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b<n. \<forall>a1<n. \<forall>a2<n. (R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2) = (P\<^sub>b ! b \<turnstile> a1 < a2)
[PROOF STEP]
by (simp add: P\<^sub>b_set \<open>R\<^sub>b = _\<close> length_P\<^sub>b ranking_iff_pref)
[PROOF STATE]
proof (state)
this:
\<forall>b<n. \<forall>a1<n. \<forall>a2<n. (R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2) = (P\<^sub>b ! b \<turnstile> a1 < a2)

goal (1 subgoal):
 1. (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
[PROOF STEP]
let ?M = "{<ai+1} - {a}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
[PROOF STEP]
have A: "wf A" and M: "?M \<subseteq> {<n}" and as: "a < n" and invAB: "invAB2 A B M ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.wf A &&& {<ai + 1} - {a} \<subseteq> {<n}) &&& a < n &&& invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
[PROOF STEP]
using assms(2,3)
[PROOF STATE]
proof (prove)
using this:
invar2' A B M ai a
ai < n

goal (1 subgoal):
 1. (local.wf A &&& {<ai + 1} - {a} \<subseteq> {<n}) &&& a < n &&& invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.wf A
{<ai + 1} - {a} \<subseteq> {<n}
a < n
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n

goal (1 subgoal):
 1. (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
[PROOF STEP]
have a': "B ! match A a \<in> ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B ! match A a \<in> {<ai + 1} - {a}
[PROOF STEP]
using invAB match_less_n[OF A] as \<open>M!match A a\<close>
[PROOF STATE]
proof (prove)
using this:
invAB A (\<alpha> B M) ({<ai + 1} - {a}) \<and> length B = n \<and> length M = n
?a < n \<Longrightarrow> match A ?a < n
a < n
M ! match A a

goal (1 subgoal):
 1. B ! match A a \<in> {<ai + 1} - {a}
[PROOF STEP]
by (metis \<alpha>_Some ranI)
[PROOF STATE]
proof (state)
this:
B ! match A a \<in> {<ai + 1} - {a}

goal (1 subgoal):
 1. (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
[PROOF STEP]
hence "B ! match A a < n"
[PROOF STATE]
proof (prove)
using this:
B ! match A a \<in> {<ai + 1} - {a}

goal (1 subgoal):
 1. B ! match A a < n
[PROOF STEP]
using M
[PROOF STATE]
proof (prove)
using this:
B ! match A a \<in> {<ai + 1} - {a}
{<ai + 1} - {a} \<subseteq> {<n}

goal (1 subgoal):
 1. B ! match A a < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B ! match A a < n

goal (1 subgoal):
 1. (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
B ! match A a < n

goal (1 subgoal):
 1. (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
[PROOF STEP]
using assms R match_less_n
[PROOF STATE]
proof (prove)
using this:
B ! match A a < n
R\<^sub>b = map ranking P\<^sub>b
invar2' A B M ai a
ai < n
M ! match A a
\<forall>b<n. \<forall>a1<n. \<forall>a2<n. (R\<^sub>b ! b ! a1 < R\<^sub>b ! b ! a2) = (P\<^sub>b ! b \<turnstile> a1 < a2)
\<lbrakk>local.wf ?A; ?a < n\<rbrakk> \<Longrightarrow> match ?A ?a < n

goal (1 subgoal):
 1. (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Gale_Shapley6_1:
assumes "R\<^sub>b = map ranking P\<^sub>b"
shows "VARS A B M a a' ai b r
 [ai = 0 \<and> a = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False]
 WHILE ai < n
 INV { invar2' A B M ai a }
 VAR {var A ({<ai+1} - {a})}
 DO b := match A a;
  IF \<not> M ! b
  THEN B[b] := a; M[b] := True; ai := ai + 1; a := ai
  ELSE a' := B ! b; r := R\<^sub>b ! match A a';
       IF r ! a < r ! a'
       THEN B[b] := a; A[a'] := A!a'+1; a := a'
       ELSE A[a] := A!a+1
       FI
  FI
 OD
 [matching A {<n} \<and> stable A {<n} \<and> opti\<^sub>a A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [ai = 0 \<and> a = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False]
WHILE ai < n INV {invar2' A B M ai a}  VAR {var A ({<ai + 1} - {a})}
DO b := match A a; IF \<not> M ! b THEN B := B[b := a]; M := M[b := True]; ai := ai + 1; a := ai  ELSE a' := B ! b; r := R\<^sub>b ! match A a'; IF r ! a < r ! a' THEN B := B[b := a]; A := A[a' := A ! a' + 1]; a := a'  ELSE A := A[a := A ! a + 1] FI FI OD
[matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A]
[PROOF STEP]
proof (vcg_tc, goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A B M a a' ai b r. ai = 0 \<and> a = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False \<Longrightarrow> invar2' A B M ai a
 2. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
 3. \<And>A B M a a' ai b r. invar2' A B M ai a \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
ai_ = 0 \<and> a_ = 0 \<and> A_ = replicate n 0 \<and> length B_ = n \<and> M_ = replicate n False

goal (3 subgoals):
 1. \<And>A B M a a' ai b r. ai = 0 \<and> a = 0 \<and> A = replicate n 0 \<and> length B = n \<and> M = replicate n False \<Longrightarrow> invar2' A B M ai a
 2. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
 3. \<And>A B M a a' ai b r. invar2' A B M ai a \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ai_ = 0 \<and> a_ = 0 \<and> A_ = replicate n 0 \<and> length B_ = n \<and> M_ = replicate n False

goal (1 subgoal):
 1. invar2' A_ B_ M_ ai_ a_
[PROOF STEP]
by(auto simp: pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def opti\<^sub>a_def \<alpha>_def cong: conj_cong)
[PROOF STATE]
proof (state)
this:
invar2' A_ B_ M_ ai_ a_

goal (2 subgoals):
 1. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
 2. \<And>A B M a a' ai b r. invar2' A B M ai a \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
 2. \<And>A B M a a' ai b r. invar2' A B M ai a \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
invar2' A_ B_ M_ ai_ a_ \<and> \<not> ai_ < n

goal (2 subgoals):
 1. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
 2. \<And>A B M a a' ai b r. invar2' A B M ai a \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
invar2' A_ B_ M_ ai_ a_ \<and> \<not> ai_ < n

goal (1 subgoal):
 1. matching A_ {<n} \<and> local.stable A_ {<n} \<and> opti\<^sub>a A_
[PROOF STEP]
using pref_match_stable atLeast0_lessThan_Suc
[PROOF STATE]
proof (prove)
using this:
invar2' A_ B_ M_ ai_ a_ \<and> \<not> ai_ < n
\<lbrakk>matching ?A {<n}; pref_match ?A {<n}\<rbrakk> \<Longrightarrow> local.stable ?A {<n}
{<Suc ?n} = {?n} \<union> {<?n}

goal (1 subgoal):
 1. matching A_ {<n} \<and> local.stable A_ {<n} \<and> opti\<^sub>a A_
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
matching A_ {<n} \<and> local.stable A_ {<n} \<and> opti\<^sub>a A_

goal (1 subgoal):
 1. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
[PROOF STEP]
case (2 v A B M a a' ai)
[PROOF STATE]
proof (state)
this:
(invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = v

goal (1 subgoal):
 1. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
[PROOF STEP]
have R': "M ! match A a \<Longrightarrow>
    (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) =
     (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
[PROOF STEP]
using R_iff_P 2 assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?R\<^sub>b = map ranking P\<^sub>b; invar2' ?A ?B ?M ?ai ?a; ?ai < n; ?M ! match ?A ?a\<rbrakk> \<Longrightarrow> (?R\<^sub>b ! match ?A (?B ! match ?A ?a) ! ?a < ?R\<^sub>b ! match ?A (?B ! match ?A ?a) ! (?B ! match ?A ?a)) = (P\<^sub>b ! match ?A (?B ! match ?A ?a) \<turnstile> ?a < ?B ! match ?A ?a)
(invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = v
R\<^sub>b = map ranking P\<^sub>b

goal (1 subgoal):
 1. M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)

goal (1 subgoal):
 1. \<And>na A B M a a' ai b r. (invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = na \<Longrightarrow> (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < na)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r_) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)))
[PROOF STEP]
apply(simp only:mem_Collect_eq prod.case)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> M ! match A a \<longrightarrow> invar2' A (B[match A a := a]) (M[match A a := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> invar2' (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a) \<and> var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {B ! match A a}) < v) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> invar2' (A[a := A ! a + 1]) B M ai a \<and> var (A[a := A ! a + 1]) ({<ai + 1} - {a}) < v))
[PROOF STEP]
using 2 R' pres2'[of A B M ai a]
[PROOF STATE]
proof (prove)
using this:
(invar2' A B M ai a \<and> ai < n) \<and> var A ({<ai + 1} - {a}) = v
M ! match A a \<Longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a)) = (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a)
\<lbrakk>invar2' A B M ai a; ai < n; var A ({<ai + 1} - {a}) = ?v; ?b = match A a; ?a' = B ! ?b; ?A1.0 = A[?a' := A ! ?a' + 1]; ?A2.0 = A[a := A ! a + 1]\<rbrakk> \<Longrightarrow> (\<not> M ! ?b \<longrightarrow> invar2' A (B[?b := a]) (M[?b := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < ?v) \<and> (M ! ?b \<longrightarrow> (P\<^sub>b ! match A ?a' \<turnstile> a < ?a' \<longrightarrow> invar2' ?A1.0 (B[?b := a]) M ai ?a' \<and> var ?A1.0 ({<ai + 1} - {?a'}) < ?v) \<and> (\<not> P\<^sub>b ! match A ?a' \<turnstile> a < ?a' \<longrightarrow> invar2' ?A2.0 B M ai a \<and> var ?A2.0 ({<ai + 1} - {a}) < ?v))

goal (1 subgoal):
 1. (\<not> M ! match A a \<longrightarrow> invar2' A (B[match A a := a]) (M[match A a := True]) (ai + 1) (ai + 1) \<and> var A ({<ai + 1 + 1} - {ai + 1}) < v) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> invar2' (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a]) M ai (B ! match A a) \<and> var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<ai + 1} - {B ! match A a}) < v) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> invar2' (A[a := A ! a + 1]) B M ai a \<and> var (A[a := A ! a + 1]) ({<ai + 1} - {a}) < v))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
(\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], ai + 1, a', ai + 1, match A a, r_) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, B ! match A a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)) \<and> (\<not> R\<^sub>b ! match A (B ! match A a) ! a < R\<^sub>b ! match A (B ! match A a) ! (B ! match A a) \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, ai, match A a, R\<^sub>b ! match A (B ! match A a)) \<in> _Collect s ((case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> invar2' A B M ai a) \<and> (case s of (A, B, M, a, a', ai, b, r) \<Rightarrow> var A ({<ai + 1} - {a})) < v)))

goal:
No subgoals!
[PROOF STEP]
qed