[STATEMENT]
lemma Gale_Shapley1: "VARS M A a a'
 [M = {} \<and> A = replicate n 0]
 WHILE M \<noteq> {<n}
 INV { invAM A M }
 VAR {var A M}
 DO a := (SOME a. a < n \<and> a \<notin> M);
  IF match A a \<notin> match A ` M
  THEN M := M \<union> {a}
  ELSE a' := (SOME a'. a' \<in> M \<and> match A a' = match A a);
       IF P\<^sub>b ! match A a' \<turnstile> a < a'
       THEN A[a'] := A!a'+1; M := M - {a'} \<union> {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. [M = {} \<and> A = replicate n 0]
WHILE M \<noteq> {<n} INV {invAM A M}  VAR {var A M}
DO a := (SOME a. a < n \<and> a \<notin> M); IF match A a \<notin> match A ` M THEN M := M \<union> {a}  ELSE a' := (SOME a'. a' \<in> M \<and> match A a' = match A a); IF P\<^sub>b ! match A a' \<turnstile> a < a' THEN A := A[a' := A ! a' + 1]; M := M - {a'} \<union> {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>M A a a'. M = {} \<and> A = replicate n 0 \<Longrightarrow> invAM A M
 2. \<And>na M A a a'. (invAM A M \<and> M \<noteq> {<n}) \<and> var A M = na \<Longrightarrow> (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)))
 3. \<And>M A a a'. invAM A M \<and> \<not> M \<noteq> {<n} \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
M_ = {} \<and> A_ = replicate n 0

goal (3 subgoals):
 1. \<And>M A a a'. M = {} \<and> A = replicate n 0 \<Longrightarrow> invAM A M
 2. \<And>na M A a a'. (invAM A M \<and> M \<noteq> {<n}) \<and> var A M = na \<Longrightarrow> (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)))
 3. \<And>M A a a'. invAM A M \<and> \<not> M \<noteq> {<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:
M_ = {} \<and> A_ = replicate n 0

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

goal (2 subgoals):
 1. \<And>na M A a a'. (invAM A M \<and> M \<noteq> {<n}) \<and> var A M = na \<Longrightarrow> (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)))
 2. \<And>M A a a'. invAM A M \<and> \<not> M \<noteq> {<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 M A a a'. (invAM A M \<and> M \<noteq> {<n}) \<and> var A M = na \<Longrightarrow> (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)))
 2. \<And>M A a a'. invAM A M \<and> \<not> M \<noteq> {<n} \<Longrightarrow> matching A {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
invAM A_ M_ \<and> \<not> M_ \<noteq> {<n}

goal (2 subgoals):
 1. \<And>na M A a a'. (invAM A M \<and> M \<noteq> {<n}) \<and> var A M = na \<Longrightarrow> (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)))
 2. \<And>M A a a'. invAM A M \<and> \<not> M \<noteq> {<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_ M_ \<and> \<not> M_ \<noteq> {<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_ M_ \<and> \<not> M_ \<noteq> {<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 auto
[PROOF STATE]
proof (state)
this:
matching A_ {<n} \<and> local.stable A_ {<n} \<and> opti\<^sub>a A_

goal (1 subgoal):
 1. \<And>na M A a a'. (invAM A M \<and> M \<noteq> {<n}) \<and> var A M = na \<Longrightarrow> (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na M A a a'. (invAM A M \<and> M \<noteq> {<n}) \<and> var A M = na \<Longrightarrow> (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)))
[PROOF STEP]
case (2 v M A a)
[PROOF STATE]
proof (state)
this:
(invAM A M \<and> M \<noteq> {<n}) \<and> var A M = v

goal (1 subgoal):
 1. \<And>na M A a a'. (invAM A M \<and> M \<noteq> {<n}) \<and> var A M = na \<Longrightarrow> (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)))
[PROOF STEP]
hence invAM: "invAM A M" and m: "matching A M" and M: "M \<subseteq> {<n}" "M \<noteq> {<n}"
    and pref_match: "pref_match A M" and "opti\<^sub>a A" and v: "var A M = v"
[PROOF STATE]
proof (prove)
using this:
(invAM A M \<and> M \<noteq> {<n}) \<and> var A M = v

goal (1 subgoal):
 1. (invAM A M &&& matching A M &&& M \<subseteq> {<n} &&& M \<noteq> {<n}) &&& pref_match A M &&& opti\<^sub>a A &&& var A M = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invAM A M
matching A M
M \<subseteq> {<n}
M \<noteq> {<n}
pref_match A M
opti\<^sub>a A
var A M = v

goal (1 subgoal):
 1. \<And>na M A a a'. (invAM A M \<and> M \<noteq> {<n}) \<and> var A M = na \<Longrightarrow> (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)))
[PROOF STEP]
note Ainj = conj12[OF m[unfolded matching_def]]
[PROOF STATE]
proof (state)
this:
local.wf A
inj_on (match A) M

goal (1 subgoal):
 1. \<And>na M A a a'. (invAM A M \<and> M \<noteq> {<n}) \<and> var A M = na \<Longrightarrow> (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)))
[PROOF STEP]
note pref_match' = pref_match[THEN pref_match'_iff[OF Ainj(1), THEN iffD2]]
[PROOF STATE]
proof (state)
this:
pref_match' A M

goal (1 subgoal):
 1. \<And>na M A a a'. (invAM A M \<and> M \<noteq> {<n}) \<and> var A M = na \<Longrightarrow> (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < 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 M

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

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

goal (1 subgoal):
 1. \<And>na M A a a'. (invAM A M \<and> M \<noteq> {<n}) \<and> var A M = na \<Longrightarrow> (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)))
[PROOF STEP]
define a where "a = (SOME a. a < n \<and> a \<notin> M)"
[PROOF STATE]
proof (state)
this:
a = (SOME a. a < n \<and> a \<notin> M)

goal (1 subgoal):
 1. \<And>na M A a a'. (invAM A M \<and> M \<noteq> {<n}) \<and> var A M = na \<Longrightarrow> (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)))
[PROOF STEP]
have a: "a < n \<and> a \<notin> M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < n \<and> a \<notin> M
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME a. a < n \<and> a \<notin> M) < n \<and> (SOME a. a < n \<and> a \<notin> M) \<notin> M
[PROOF STEP]
using M
[PROOF STATE]
proof (prove)
using this:
M \<subseteq> {<n}
M \<noteq> {<n}

goal (1 subgoal):
 1. (SOME a. a < n \<and> a \<notin> M) < n \<and> (SOME a. a < n \<and> a \<notin> M) \<notin> M
[PROOF STEP]
by (metis (no_types, lifting) atLeastLessThan_iff someI_ex subsetI subset_antisym)
[PROOF STATE]
proof (state)
this:
a < n \<and> a \<notin> M

goal (1 subgoal):
 1. \<And>na M A a a'. (invAM A M \<and> M \<noteq> {<n}) \<and> var A M = na \<Longrightarrow> (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < na)))
[PROOF STEP]
show ?case (is "?P((SOME a. a < n \<and> a \<notin> M))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a'_) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)))
[PROOF STEP]
unfolding a_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (match A a \<notin> match A ` M \<longrightarrow> (M \<union> {a}, A, a, a'_) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> match A a \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A a} \<union> {a}, A[SOME a'. a' \<in> M \<and> match A a' = match A a := A ! (SOME a'. a' \<in> M \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M, A[a := A ! a + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (match A a \<notin> match A ` M \<longrightarrow> (M \<union> {a}, A, a, a'_) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> match A a \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A a} \<union> {a}, A[SOME a'. a' \<in> M \<and> match A a' = match A a := A ! (SOME a'. a' \<in> M \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M, A[a := A ! a + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)))
[PROOF STEP]
show "?P a" (is "(?not_matched \<longrightarrow> ?THEN) \<and> (\<not> ?not_matched \<longrightarrow> ?ELSE)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (match A a \<notin> match A ` M \<longrightarrow> (M \<union> {a}, A, a, a'_) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> match A a \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A a} \<union> {a}, A[SOME a'. a' \<in> M \<and> match A a' = match A a := A ! (SOME a'. a' \<in> M \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M, A[a := A ! a + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)))
[PROOF STEP]
proof (rule; rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. match A a \<notin> match A ` M \<Longrightarrow> (M \<union> {a}, A, a, a'_) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)
 2. \<not> match A a \<notin> match A ` M \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A a} \<union> {a}, A[SOME a'. a' \<in> M \<and> match A a' = match A a := A ! (SOME a'. a' \<in> M \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M, A[a := A ! a + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v))
[PROOF STEP]
assume ?not_matched
[PROOF STATE]
proof (state)
this:
match A a \<notin> match A ` M

goal (2 subgoals):
 1. match A a \<notin> match A ` M \<Longrightarrow> (M \<union> {a}, A, a, a'_) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)
 2. \<not> match A a \<notin> match A ` M \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A a} \<union> {a}, A[SOME a'. a' \<in> M \<and> match A a' = match A a := A ! (SOME a'. a' \<in> M \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M, A[a := A ! a + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v))
[PROOF STEP]
show ?THEN
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M \<union> {a}, A, a, a'_) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < 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 (M \<union> {a})
 2. var A (M \<union> {a}) < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invAM A (M \<union> {a})
 2. var A (M \<union> {a}) < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM A (M \<union> {a})
[PROOF STEP]
using invAM_match[OF invAM a \<open>?not_matched\<close>]
[PROOF STATE]
proof (prove)
using this:
invAM A (M \<union> {a})

goal (1 subgoal):
 1. invAM A (M \<union> {a})
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
invAM A (M \<union> {a})

goal (1 subgoal):
 1. var A (M \<union> {a}) < v
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. var A (M \<union> {a}) < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var A (M \<union> {a}) < v
[PROOF STEP]
using var_match[OF m M pref_match1] var0_match[OF Ainj(1) M(1)] a
[PROOF STATE]
proof (prove)
using this:
?a \<notin> M \<Longrightarrow> var A (M \<union> {?a}) < var A M
?a < n \<and> ?a \<notin> M \<Longrightarrow> var0 A (M \<union> {?a}) < var0 A M
a < n \<and> a \<notin> M

goal (1 subgoal):
 1. var A (M \<union> {a}) < v
[PROOF STEP]
unfolding v
[PROOF STATE]
proof (prove)
using this:
?a \<notin> M \<Longrightarrow> var A (M \<union> {?a}) < v
?a < n \<and> ?a \<notin> M \<Longrightarrow> var0 A (M \<union> {?a}) < var0 A M
a < n \<and> a \<notin> M

goal (1 subgoal):
 1. var A (M \<union> {a}) < v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
var A (M \<union> {a}) < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(M \<union> {a}, A, a, a'_) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)

goal (1 subgoal):
 1. \<not> match A a \<notin> match A ` M \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A a} \<union> {a}, A[SOME a'. a' \<in> M \<and> match A a' = match A a := A ! (SOME a'. a' \<in> M \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M, A[a := A ! a + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> match A a \<notin> match A ` M \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A a} \<union> {a}, A[SOME a'. a' \<in> M \<and> match A a' = match A a := A ! (SOME a'. a' \<in> M \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M, A[a := A ! a + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v))
[PROOF STEP]
assume matched: "\<not> ?not_matched"
[PROOF STATE]
proof (state)
this:
\<not> match A a \<notin> match A ` M

goal (1 subgoal):
 1. \<not> match A a \<notin> match A ` M \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A a} \<union> {a}, A[SOME a'. a' \<in> M \<and> match A a' = match A a := A ! (SOME a'. a' \<in> M \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M, A[a := A ! a + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v))
[PROOF STEP]
define a' where "a' = (SOME a'.  a' \<in> M \<and> match A a' = match A a)"
[PROOF STATE]
proof (state)
this:
a' = (SOME a'. a' \<in> M \<and> match A a' = match A a)

goal (1 subgoal):
 1. \<not> match A a \<notin> match A ` M \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A a} \<union> {a}, A[SOME a'. a' \<in> M \<and> match A a' = match A a := A ! (SOME a'. a' \<in> M \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M, A[a := A ! a + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v))
[PROOF STEP]
have a': "a' \<in> M \<and> match A a' = match A a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a' \<in> M \<and> match A a' = match A a
[PROOF STEP]
unfolding a'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> M \<and> match A (SOME a'. a' \<in> M \<and> match A a' = match A a) = match A a
[PROOF STEP]
using matched
[PROOF STATE]
proof (prove)
using this:
\<not> match A a \<notin> match A ` M

goal (1 subgoal):
 1. (SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> M \<and> match A (SOME a'. a' \<in> M \<and> match A a' = match A a) = match A a
[PROOF STEP]
by (smt (verit) image_iff someI_ex)
[PROOF STATE]
proof (state)
this:
a' \<in> M \<and> match A a' = match A a

goal (1 subgoal):
 1. \<not> match A a \<notin> match A ` M \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A a} \<union> {a}, A[SOME a'. a' \<in> M \<and> match A a' = match A a := A ! (SOME a'. a' \<in> M \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M, A[a := A ! a + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v))
[PROOF STEP]
hence "a' < n" "a \<noteq> a'"
[PROOF STATE]
proof (prove)
using this:
a' \<in> M \<and> match A a' = match A a

goal (1 subgoal):
 1. a' < n &&& a \<noteq> a'
[PROOF STEP]
using a M atLeast0LessThan
[PROOF STATE]
proof (prove)
using this:
a' \<in> M \<and> match A a' = match A a
a < n \<and> a \<notin> M
M \<subseteq> {<n}
M \<noteq> {<n}
{<?n} = {..<?n}

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

goal (1 subgoal):
 1. \<not> match A a \<notin> match A ` M \<Longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A a} \<union> {a}, A[SOME a'. a' \<in> M \<and> match A a' = match A a := A ! (SOME a'. a' \<in> M \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M, A[a := A ! a + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v))
[PROOF STEP]
show ?ELSE (is "?P((SOME a'. a' \<in> M \<and> match A a' = match A a))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A a} \<union> {a}, A[SOME a'. a' \<in> M \<and> match A a' = match A a := A ! (SOME a'. a' \<in> M \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M, A[a := A ! a + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v))
[PROOF STEP]
unfolding a'_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (M - {a'} \<union> {a}, A[a' := A ! a' + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (M, A[a := A ! a + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (M - {a'} \<union> {a}, A[a' := A ! a' + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (M, A[a := A ! a + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v))
[PROOF STEP]
show "?P a'" (is "(?pref \<longrightarrow> ?THEN) \<and> (\<not> ?pref \<longrightarrow> ?ELSE)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (M - {a'} \<union> {a}, A[a' := A ! a' + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<longrightarrow> (M, A[a := A ! a + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v))
[PROOF STEP]
proof (rule; rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (M - {a'} \<union> {a}, A[a' := A ! a' + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)
 2. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (M, A[a := A ! a + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)
[PROOF STEP]
assume ?pref
[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> (M - {a'} \<union> {a}, A[a' := A ! a' + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)
 2. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (M, A[a := A ! a + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)
[PROOF STEP]
show ?THEN
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M - {a'} \<union> {a}, A[a' := A ! a' + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < 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]) (M - {a'} \<union> {a})
 2. var (A[a' := A ! a' + 1]) (M - {a'} \<union> {a}) < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
 2. var (A[a' := A ! a' + 1]) (M - {a'} \<union> {a}) < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
by(rule invAM_swap[OF invAM a a' \<open>?pref\<close>])
[PROOF STATE]
proof (state)
this:
invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})

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

goal (1 subgoal):
 1. var (A[a' := A ! a' + 1]) (M - {a'} \<union> {a}) < v
[PROOF STEP]
have "card(M - {a'} \<union> {a}) = card M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (M - {a'} \<union> {a}) = card M
[PROOF STEP]
using a a' card.remove subset_eq_atLeast0_lessThan_finite[OF M(1)]
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> M
a' \<in> M \<and> match A a' = match A a
\<lbrakk>finite ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> card ?A = Suc (card (?A - {?x}))
finite M

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

goal (1 subgoal):
 1. var (A[a' := A ! a' + 1]) (M - {a'} \<union> {a}) < v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
card (M - {a'} \<union> {a}) = card M

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

goal (1 subgoal):
 1. var (A[a' := A ! a' + 1]) (M - {a'} \<union> {a}) < v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
var (A[a' := A ! a' + 1]) (M - {a'} \<union> {a}) < v

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

goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (M, A[a := A ! a + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A a' \<turnstile> a < a' \<Longrightarrow> (M, A[a := A ! a + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)
[PROOF STEP]
assume "\<not> ?pref"
[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> (M, A[a := A ! a + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)
[PROOF STEP]
show ?ELSE
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, A[a := A ! a + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < 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]) M
 2. var (A[a := A ! a + 1]) M < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invAM (A[a := A ! a + 1]) M
 2. var (A[a := A ! a + 1]) M < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
using invAM_next[OF invAM a a' \<open>\<not> ?pref\<close>]
[PROOF STATE]
proof (prove)
using this:
invAM (A[a := A ! a + 1]) M

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
invAM (A[a := A ! a + 1]) M

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

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) M < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var (A[a := A ! a + 1]) M < v
[PROOF STEP]
using a v var_next[OF m M pref_match1, of a] var0_next[OF Ainj(1) M, of a]
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> M
var A M = v
a < n \<Longrightarrow> var (A[a := A ! a + 1]) M < var A M
a < n \<Longrightarrow> var0 (A[a := A ! a + 1]) M < var0 A M

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) M < v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
var (A[a := A ! a + 1]) M < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(M, A[a := A ! a + 1], a, a') \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(match A a \<notin> match A ` M \<longrightarrow> (M \<union> {a}, A, a, a'_) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> match A a \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A a} \<union> {a}, A[SOME a'. a' \<in> M \<and> match A a' = match A a := A ! (SOME a'. a' \<in> M \<and> match A a' = match A a) + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A a) \<turnstile> a < (SOME a'. a' \<in> M \<and> match A a' = match A a) \<longrightarrow> (M, A[a := A ! a + 1], a, SOME a'. a' \<in> M \<and> match A a' = match A a) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (M \<union> {SOME a. a < n \<and> a \<notin> M}, A, SOME a. a < n \<and> a \<notin> M, a'_) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> match A (SOME a. a < n \<and> a \<notin> M) \<notin> match A ` M \<longrightarrow> (P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M - {SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)} \<union> {SOME a. a < n \<and> a \<notin> M}, A[SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M) := A ! (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)) \<and> (\<not> P\<^sub>b ! match A (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<turnstile> (SOME a. a < n \<and> a \<notin> M) < (SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<longrightarrow> (M, A[SOME a. a < n \<and> a \<notin> M := A ! (SOME a. a < n \<and> a \<notin> M) + 1], SOME a. a < n \<and> a \<notin> M, SOME a'. a' \<in> M \<and> match A a' = match A (SOME a. a < n \<and> a \<notin> M)) \<in> _Collect s ((case s of (M, A, a, a') \<Rightarrow> invAM A M) \<and> (case s of (M, A, a, a') \<Rightarrow> var A M) < v)))

goal:
No subgoals!
[PROOF STEP]
qed