[STATEMENT]
lemma Gale_Shapley4:
"VARS A B ai a a'
 [ai = 0 \<and> A = replicate n 0 \<and> B = (\<lambda>_. None)]
 WHILE ai < n
 INV { invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n }
 VAR {z = n - ai}
 DO a := ai;
  WHILE B (match A a) \<noteq> None
  INV { invAM A ({<ai+1} - {a}) \<and> invAB A B ({<ai+1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n-ai }
  VAR {var A {<ai}}
  DO a' := the(B (match A a));
     IF P\<^sub>b ! match A a' \<turnstile> a < a'
     THEN B := B(match A a := Some a); A[a'] := A!a'+1; a := a'
     ELSE A[a] := A!a+1
     FI
  OD;
  B := B(match A a := Some a); 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> B = Map.empty]
WHILE ai < n INV {invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n}  VAR {z = n - ai}
DO a := ai; WHILE B (match A a) \<noteq> None INV {invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai}  VAR {var A {<ai}}
DO a' := the (B (match A a)); IF P\<^sub>b ! match A a' \<turnstile> a < a' THEN B := B(match A a \<mapsto> a); A := A[a' := A ! a' + 1]; a := a'  ELSE A := A[a := A ! a + 1] FI OD; B := B(match A a \<mapsto> a); 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 ai a a'. ai = 0 \<and> A = replicate n 0 \<and> B = Map.empty \<Longrightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n
 2. \<And>z A B ai a a'. ((invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invAM A ({<ai + 1} - {ai}) \<and> invAB A B ({<ai + 1} - {ai}) \<and> (ai \<le> ai \<and> ai < n) \<and> z = n - ai
 3. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 4. \<And>z A B ai a a'. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> n - ai) < z)
 5. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<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> B_ = Map.empty

goal (5 subgoals):
 1. \<And>A B ai a a'. ai = 0 \<and> A = replicate n 0 \<and> B = Map.empty \<Longrightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n
 2. \<And>z A B ai a a'. ((invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invAM A ({<ai + 1} - {ai}) \<and> invAB A B ({<ai + 1} - {ai}) \<and> (ai \<le> ai \<and> ai < n) \<and> z = n - ai
 3. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 4. \<And>z A B ai a a'. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> n - ai) < z)
 5. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<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> B_ = Map.empty

goal (1 subgoal):
 1. invAM A_ {<ai_} \<and> invAB A_ B_ {<ai_} \<and> ai_ \<le> n
[PROOF STEP]
(* outer invar holds initially *)
[PROOF STATE]
proof (prove)
using this:
ai_ = 0 \<and> A_ = replicate n 0 \<and> B_ = Map.empty

goal (1 subgoal):
 1. invAM A_ {<ai_} \<and> invAB A_ B_ {<ai_} \<and> ai_ \<le> n
[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)[]
[PROOF STATE]
proof (state)
this:
invAM A_ {<ai_} \<and> invAB A_ B_ {<ai_} \<and> ai_ \<le> n

goal (4 subgoals):
 1. \<And>z A B ai a a'. ((invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invAM A ({<ai + 1} - {ai}) \<and> invAB A B ({<ai + 1} - {ai}) \<and> (ai \<le> ai \<and> ai < n) \<and> z = n - ai
 2. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 3. \<And>z A B ai a a'. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> n - ai) < z)
 4. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<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 ai a a'. ((invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invAM A ({<ai + 1} - {ai}) \<and> invAB A B ({<ai + 1} - {ai}) \<and> (ai \<le> ai \<and> ai < n) \<and> z = n - ai
 2. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 3. \<And>z A B ai a a'. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> n - ai) < z)
 4. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<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:
((invAM A_ {<ai_} \<and> invAB A_ B_ {<ai_} \<and> ai_ \<le> n) \<and> ai_ < n) \<and> n - ai_ = z_

goal (4 subgoals):
 1. \<And>z A B ai a a'. ((invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invAM A ({<ai + 1} - {ai}) \<and> invAB A B ({<ai + 1} - {ai}) \<and> (ai \<le> ai \<and> ai < n) \<and> z = n - ai
 2. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 3. \<And>z A B ai a a'. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> n - ai) < z)
 4. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<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:
((invAM A_ {<ai_} \<and> invAB A_ B_ {<ai_} \<and> ai_ \<le> n) \<and> ai_ < n) \<and> n - ai_ = z_

goal (4 subgoals):
 1. \<And>z A B ai a a'. ((invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> ai < n) \<and> n - ai = z \<Longrightarrow> invAM A ({<ai + 1} - {ai}) \<and> invAB A B ({<ai + 1} - {ai}) \<and> (ai \<le> ai \<and> ai < n) \<and> z = n - ai
 2. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 3. \<And>z A B ai a a'. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> n - ai) < z)
 4. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<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:
((invAM A_ {<ai_} \<and> invAB A_ B_ {<ai_} \<and> ai_ \<le> n) \<and> ai_ < n) \<and> n - ai_ = z_

goal (1 subgoal):
 1. invAM A_ ({<ai_ + 1} - {ai_}) \<and> invAB A_ B_ ({<ai_ + 1} - {ai_}) \<and> (ai_ \<le> ai_ \<and> ai_ < n) \<and> z_ = n - ai_
[PROOF STEP]
by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff)
[PROOF STATE]
proof (state)
this:
invAM A_ ({<ai_ + 1} - {ai_}) \<and> invAB A_ B_ ({<ai_ + 1} - {ai_}) \<and> (ai_ \<le> ai_ \<and> ai_ < n) \<and> z_ = n - ai_

goal (3 subgoals):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>z A B ai a a'. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> n - ai) < z)
 3. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<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 ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>z A B ai a a'. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> n - ai) < z)
 3. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case (4 z A B ai a)
[PROOF STATE]
proof (state)
this:
(invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None

goal (3 subgoals):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>z A B ai a a'. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> n - ai) < z)
 3. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<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:
(invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None

goal (3 subgoals):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>z A B ai a a'. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> n - ai) < z)
 3. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
note inv = 4[THEN conjunct1]
[PROOF STATE]
proof (state)
this:
invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai

goal (3 subgoals):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>z A B ai a a'. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> n - ai) < z)
 3. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
note invAM = inv[THEN conjunct1]
[PROOF STATE]
proof (state)
this:
invAM A ({<ai + 1} - {a})

goal (3 subgoals):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>z A B ai a a'. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> n - ai) < z)
 3. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> \<not> ai < n \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
note aai = inv[THEN conjunct2,THEN conjunct2]
[PROOF STATE]
proof (state)
this:
(a \<le> ai \<and> ai < n) \<and> z = n - ai

goal (3 subgoals):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>z A B ai a a'. (invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None \<Longrightarrow> (A, B(match A a \<mapsto> a), ai + 1, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> n - ai) < z)
 3. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<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(match A a \<mapsto> a), ai + 1, a, a'_) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<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. invAM A {<ai + 1} \<and> invAB A (B(match A a \<mapsto> a)) {<ai + 1} \<and> ai + 1 \<le> n
 2. n - (ai + 1) < z
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invAM A {<ai + 1} \<and> invAB A (B(match A a \<mapsto> a)) {<ai + 1} \<and> ai + 1 \<le> n
 2. n - (ai + 1) < z
[PROOF STEP]
have *: "{<Suc ai} = insert a ({<Suc ai} - {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<Suc ai} = {a} \<union> ({<Suc ai} - {a})
[PROOF STEP]
using aai
[PROOF STATE]
proof (prove)
using this:
(a \<le> ai \<and> ai < n) \<and> z = n - ai

goal (1 subgoal):
 1. {<Suc ai} = {a} \<union> ({<Suc ai} - {a})
[PROOF STEP]
by (simp add: insert_absorb)
[PROOF STATE]
proof (state)
this:
{<Suc ai} = {a} \<union> ({<Suc ai} - {a})

goal (2 subgoals):
 1. invAM A {<ai + 1} \<and> invAB A (B(match A a \<mapsto> a)) {<ai + 1} \<and> ai + 1 \<le> n
 2. n - (ai + 1) < z
[PROOF STEP]
have **: "inj_on (match A) {<Suc ai} = (inj_on (match A) ({<Suc ai} - {a}) \<and> match A a \<notin> match A ` ({<Suc ai} - {a}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (match A) {<Suc ai} = (inj_on (match A) ({<Suc ai} - {a}) \<and> match A a \<notin> match A ` ({<Suc ai} - {a}))
[PROOF STEP]
by (metis "*" Diff_idemp inj_on_insert)
[PROOF STATE]
proof (state)
this:
inj_on (match A) {<Suc ai} = (inj_on (match A) ({<Suc ai} - {a}) \<and> match A a \<notin> match A ` ({<Suc ai} - {a}))

goal (2 subgoals):
 1. invAM A {<ai + 1} \<and> invAB A (B(match A a \<mapsto> a)) {<ai + 1} \<and> ai + 1 \<le> n
 2. n - (ai + 1) < z
[PROOF STEP]
have nm: "match A a \<notin> match A ` ({<Suc ai} - {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match A a \<notin> match A ` ({<Suc ai} - {a})
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
(invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None

goal (1 subgoal):
 1. match A a \<notin> match A ` ({<Suc ai} - {a})
[PROOF STEP]
unfolding ran_def
[PROOF STATE]
proof (prove)
using this:
(invAM A ({<ai + 1} - {a}) \<and> (_Collect b (\<exists>a. B a = Some b) = {<ai + 1} - {a} \<and> (\<forall>b a. B b = Some a \<longrightarrow> match A a = b)) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None

goal (1 subgoal):
 1. match A a \<notin> match A ` ({<Suc ai} - {a})
[PROOF STEP]
apply (clarsimp simp: set_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>n = length A; set A \<subseteq> {<length A}; inj_on (match A) ({<Suc ai} - {a}); {<Suc ai} - {a} \<subseteq> {<length A}; pref_match A ({<Suc ai} - {a}); opti\<^sub>a A; \<forall>x. (\<exists>a. B a = Some x) = (x < Suc ai \<and> x \<noteq> a); \<forall>b a. B b = Some a \<longrightarrow> match A a = b; a \<le> ai; ai < length A; z = length A - ai; B (match A x) = None; match A a = match A x; x < Suc ai\<rbrakk> \<Longrightarrow> x = a
[PROOF STEP]
by (metis not_None_eq)
[PROOF STATE]
proof (state)
this:
match A a \<notin> match A ` ({<Suc ai} - {a})

goal (2 subgoals):
 1. invAM A {<ai + 1} \<and> invAB A (B(match A a \<mapsto> a)) {<ai + 1} \<and> ai + 1 \<le> n
 2. n - (ai + 1) < z
[PROOF STEP]
have invAM': "invAM A {<ai+1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM A {<ai + 1}
[PROOF STEP]
using invAM_match[OF invAM, of a] aai nm
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a < n \<and> a \<notin> {<ai + 1} - {a}; match A a \<notin> match A ` ({<ai + 1} - {a})\<rbrakk> \<Longrightarrow> invAM A ({<ai + 1} - {a} \<union> {a})
(a \<le> ai \<and> ai < n) \<and> z = n - ai
match A a \<notin> match A ` ({<Suc ai} - {a})

goal (1 subgoal):
 1. invAM A {<ai + 1}
[PROOF STEP]
by (simp add: ** insert_absorb)
[PROOF STATE]
proof (state)
this:
invAM A {<ai + 1}

goal (2 subgoals):
 1. invAM A {<ai + 1} \<and> invAB A (B(match A a \<mapsto> a)) {<ai + 1} \<and> ai + 1 \<le> n
 2. n - (ai + 1) < z
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM A {<ai + 1} \<and> invAB A (B(match A a \<mapsto> a)) {<ai + 1} \<and> ai + 1 \<le> n
[PROOF STEP]
using 4 invAM'
[PROOF STATE]
proof (prove)
using this:
(invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None
invAM A {<ai + 1}

goal (1 subgoal):
 1. invAM A {<ai + 1} \<and> invAB A (B(match A a \<mapsto> a)) {<ai + 1} \<and> ai + 1 \<le> n
[PROOF STEP]
by (simp add: insert_absorb)
[PROOF STATE]
proof (state)
this:
invAM A {<ai + 1} \<and> invAB A (B(match A a \<mapsto> a)) {<ai + 1} \<and> ai + 1 \<le> n

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:
(invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> \<not> B (match A a) \<noteq> None

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(match A a \<mapsto> a), ai + 1, a, a'_) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> n - ai) < z)

goal (2 subgoals):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<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 na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<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:
(invAM A_ {<ai_} \<and> invAB A_ B_ {<ai_} \<and> ai_ \<le> n) \<and> \<not> ai_ < n

goal (2 subgoals):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<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 implies post *)
[PROOF STATE]
proof (state)
this:
(invAM A_ {<ai_} \<and> invAB A_ B_ {<ai_} \<and> ai_ \<le> n) \<and> \<not> ai_ < n

goal (2 subgoals):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
 2. \<And>A B ai a a'. (invAM A {<ai} \<and> invAB A B {<ai} \<and> ai \<le> n) \<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:
(invAM A_ {<ai_} \<and> invAB A_ B_ {<ai_} \<and> ai_ \<le> n) \<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:
(invAM A_ {<ai_} \<and> invAB A_ B_ {<ai_} \<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]
unfolding invAM_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_ B_ {<ai_} \<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 (1 subgoal):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
case (3 z v A B ai a a')
[PROOF STATE]
proof (state)
this:
((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = v

goal (1 subgoal):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
(* preservation of inner invar *)
[PROOF STATE]
proof (state)
this:
((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = v

goal (1 subgoal):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
let ?M = "{<ai+1} - {a}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
have invAM: "invAM A ?M" and m: "matching A ?M" and A: "wf A" and M: "?M \<subseteq> {<n}"
    and pref_match: "pref_match A ?M" and matched: "B(match A a) \<noteq> None" and "a \<le> ai"
    and v: "var A ?M = v" and as: "a \<le> ai \<and> ai < n" and invAB: "invAB A B ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((invAM A ({<ai + 1} - {a}) &&& matching A ({<ai + 1} - {a})) &&& local.wf A &&& {<ai + 1} - {a} \<subseteq> {<n} &&& pref_match A ({<ai + 1} - {a})) &&& (B (match A a) \<noteq> None &&& a \<le> ai) &&& var A ({<ai + 1} - {a}) = v &&& a \<le> ai \<and> ai < n &&& invAB A B ({<ai + 1} - {a})
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = v

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

goal (1 subgoal):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
note invar = 3[THEN conjunct1,THEN conjunct1]
[PROOF STATE]
proof (state)
this:
invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai

goal (1 subgoal):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[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. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[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. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
from matched
[PROOF STATE]
proof (chain)
picking this:
B (match A a) \<noteq> None
[PROOF STEP]
obtain a' where a'eq: "B(match A a) = Some a'"
[PROOF STATE]
proof (prove)
using this:
B (match A a) \<noteq> None

goal (1 subgoal):
 1. (\<And>a'. B (match A a) = Some a' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B (match A a) = Some a'

goal (1 subgoal):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
have a': "a' \<in> ?M \<and> match A a' = match A a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a' \<in> {<ai + 1} - {a} \<and> match A a' = match A a
[PROOF STEP]
using a'eq invAB
[PROOF STATE]
proof (prove)
using this:
B (match A a) = Some a'
invAB A B ({<ai + 1} - {a})

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

goal (1 subgoal):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[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 invar
[PROOF STATE]
proof (prove)
using this:
invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai

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. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
have "?M \<noteq> {<n}" and "a' < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<ai + 1} - {a} \<noteq> {<n} &&& 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}
a' \<in> {<ai + 1} - {a} \<and> match A a' = match A a
{<?n} = {..<?n}

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

goal (1 subgoal):
 1. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[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 \<open>a \<le> ai\<close>
[PROOF STATE]
proof (prove)
using this:
a \<le> ai

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. \<And>z na A B ai a a'. ((invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> B (match A a) \<noteq> None) \<and> var A {<ai} = na \<Longrightarrow> (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < na))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v))
[PROOF STEP]
unfolding a'eq option.sel
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a' := A ! a' + 1], B(match A a \<mapsto> a), ai, a', a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a := A ! a + 1], B, ai, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v))
[PROOF STEP]
proof (goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a' := A ! a' + 1], B(match A a \<mapsto> a), ai, a', a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a := A ! a + 1], B, ai, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a' := A ! a' + 1], B(match A a \<mapsto> a), ai, a', a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a := A ! a + 1], B, ai, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v))
[PROOF STEP]
show ?case (is "(?unstab \<longrightarrow> ?THEN) \<and> (\<not> ?unstab \<longrightarrow> ?ELSE)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a' := A ! a' + 1], B(match A a \<mapsto> a), ai, a', a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a := A ! a + 1], B, ai, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v))
[PROOF STEP]
proof (rule; rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a' := A ! a' + 1], B(match A a \<mapsto> a), ai, a', a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)
 2. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a := A ! a + 1], B, ai, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)
[PROOF STEP]
assume ?unstab
[PROOF STATE]
proof (state)
this:
P\<^sub>b ! match A a' \<turnstile> a < a'

goal (2 subgoals):
 1. P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a' := A ! a' + 1], B(match A a \<mapsto> a), ai, a', a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)
 2. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a := A ! a + 1], B, ai, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)
[PROOF STEP]
have *: "{<ai + 1} - {a} - {a'} \<union> {a} = {<ai + 1} - {a'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<ai + 1} - {a} - {a'} \<union> {a} = {<ai + 1} - {a'}
[PROOF STEP]
using invar a'
[PROOF STATE]
proof (prove)
using this:
invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai
a' \<in> {<ai + 1} - {a} \<and> match A a' = match A a

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

goal (2 subgoals):
 1. P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a' := A ! a' + 1], B(match A a \<mapsto> a), ai, a', a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)
 2. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a := A ! a + 1], B, ai, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)
[PROOF STEP]
show ?THEN
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A[a' := A ! a' + 1], B(match A a \<mapsto> a), ai, a', a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)
[PROOF STEP]
proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai < n) \<and> z = n - ai
 2. var (A[a' := A ! a' + 1]) {<ai} < v
[PROOF STEP]
have inj_dom: "inj_on B (dom B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on B (dom B)
[PROOF STEP]
by (metis (mono_tags) domD inj_onI invAB)
[PROOF STATE]
proof (state)
this:
inj_on B (dom B)

goal (2 subgoals):
 1. invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai < n) \<and> z = n - ai
 2. var (A[a' := A ! a' + 1]) {<ai} < v
[PROOF STEP]
have invAB': "invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'})
[PROOF STEP]
using invAB_swap[OF invAB a a' inj_dom a'eq] *
[PROOF STATE]
proof (prove)
using this:
invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a} - {a'} \<union> {a})
{<ai + 1} - {a} - {a'} \<union> {a} = {<ai + 1} - {a'}

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

goal (2 subgoals):
 1. invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai < n) \<and> z = n - ai
 2. var (A[a' := A ! a' + 1]) {<ai} < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai < n) \<and> z = n - ai
 2. var (A[a' := A ! a' + 1]) {<ai} < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai < n) \<and> z = n - ai
[PROOF STEP]
using invAM_swap[OF invAM a a' \<open>?unstab\<close>] invAB' invar a'
[PROOF STATE]
proof (prove)
using this:
invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a} - {a'} \<union> {a})
invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'})
invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai
a' \<in> {<ai + 1} - {a} \<and> match A a' = match A a

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai < n) \<and> z = n - ai
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'})
invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'})
invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai
a' \<in> {<ai + 1} - {a} \<and> match A a' = match A a

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai < n) \<and> z = n - ai
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
invAM (A[a' := A ! a' + 1]) ({<ai + 1} - {a'}) \<and> invAB (A[a' := A ! a' + 1]) (B(match A a \<mapsto> a)) ({<ai + 1} - {a'}) \<and> (a' \<le> ai \<and> ai < n) \<and> z = n - ai

goal (1 subgoal):
 1. var (A[a' := A ! a' + 1]) {<ai} < v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. var (A[a' := A ! a' + 1]) {<ai} < v
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. var (A[a' := A ! a' + 1]) {<ai} < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var (A[a' := A ! a' + 1]) {<ai} < v
[PROOF STEP]
using v var_next[OF m M \<open>?M \<noteq> {<n}\<close> pref_match1 \<open>a' < n\<close>] card
[PROOF STATE]
proof (prove)
using this:
var A ({<ai + 1} - {a}) = v
var (A[a' := A ! a' + 1]) ({<ai + 1} - {a}) < var A ({<ai + 1} - {a})
card {<ai} = card ({<ai + 1} - {a})

goal (1 subgoal):
 1. var (A[a' := A ! a' + 1]) {<ai} < v
[PROOF STEP]
by (metis var_def Suc_eq_plus1 psubset_eq)
[PROOF STATE]
proof (state)
this:
var (A[a' := A ! a' + 1]) {<ai} < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(A[a' := A ! a' + 1], B(match A a \<mapsto> a), ai, a', a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)

goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a := A ! a + 1], B, ai, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a := A ! a + 1], B, ai, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)
[PROOF STEP]
assume "\<not> ?unstab"
[PROOF STATE]
proof (state)
this:
\<not> P\<^sub>b ! match A a' \<turnstile> a < a'

goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (A[a := A ! a + 1], B, ai, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)
[PROOF STEP]
show ?ELSE
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A[a := A ! a + 1], B, ai, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)
[PROOF STEP]
proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> invAB (A[a := A ! a + 1]) B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai
 2. var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
have *: "\<forall>b a'. B b = Some a' \<longrightarrow> a \<noteq> a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b a'. B b = Some a' \<longrightarrow> a \<noteq> a'
[PROOF STEP]
by (metis invAB ranI a)
[PROOF STATE]
proof (state)
this:
\<forall>b a'. B b = Some a' \<longrightarrow> a \<noteq> a'

goal (2 subgoals):
 1. invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> invAB (A[a := A ! a + 1]) B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai
 2. var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> invAB (A[a := A ! a + 1]) B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai
 2. var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> invAB (A[a := A ! a + 1]) B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai
[PROOF STEP]
using invAM_next[OF invAM a a' \<open>\<not> ?unstab\<close>] invar *
[PROOF STATE]
proof (prove)
using this:
invAM (A[a := A ! a + 1]) ({<ai + 1} - {a})
invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai
\<forall>b a'. B b = Some a' \<longrightarrow> a \<noteq> a'

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> invAB (A[a := A ! a + 1]) B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai
[PROOF STEP]
by (simp add: match_def)
[PROOF STATE]
proof (state)
this:
invAM (A[a := A ! a + 1]) ({<ai + 1} - {a}) \<and> invAB (A[a := A ! a + 1]) B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
using v var_next[OF m M \<open>?M \<noteq> {<n}\<close> pref_match1, of a] a card
[PROOF STATE]
proof (prove)
using this:
var A ({<ai + 1} - {a}) = v
a < n \<Longrightarrow> var (A[a := A ! a + 1]) ({<ai + 1} - {a}) < var A ({<ai + 1} - {a})
a < n \<and> a \<notin> {<ai + 1} - {a}
card {<ai} = card ({<ai + 1} - {a})

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) {<ai} < v
[PROOF STEP]
by (metis Suc_eq_plus1 var_def)
[PROOF STATE]
proof (state)
this:
var (A[a := A ! a + 1]) {<ai} < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(A[a := A ! a + 1], B, ai, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a' := A ! a' + 1], B(match A a \<mapsto> a), ai, a', a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (A[a := A ! a + 1], B, ai, a, a') \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[the (B (match A a)) := A ! the (B (match A a)) + 1], B(match A a \<mapsto> a), ai, the (B (match A a)), the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v)) \<and> (\<not> P\<^sub>b ! match A (the (B (match A a))) \<turnstile> a < the (B (match A a)) \<longrightarrow> (A[a := A ! a + 1], B, ai, a, the (B (match A a))) \<in> _Collect s ((case s of (A, B, ai, a, a') \<Rightarrow> invAM A ({<ai + 1} - {a}) \<and> invAB A B ({<ai + 1} - {a}) \<and> (a \<le> ai \<and> ai < n) \<and> z = n - ai) \<and> (case s of (A, B, ai, a, a') \<Rightarrow> var A {<ai}) < v))

goal:
No subgoals!
[PROOF STEP]
qed