[STATEMENT]
lemma Gale_Shapley4_unused: "VARS A B M a a' as b
 [as = [0..<n] \<and> A = replicate n 0 \<and> B = replicate n 0 \<and> M = replicate n False]
 WHILE as \<noteq> []
 INV { invAM A ({<n} - set as) \<and> invAB' A B M ({<n} - set as) \<and> invas as}
 VAR {var A ({<n} - set as)}
 DO a := hd as; b := match A a;
  IF \<not> (M ! b)
  THEN M[b] := True; B[b] := a; as := tl as
  ELSE a' := B ! b;
       IF P\<^sub>b ! match A a' \<turnstile> a < a'
       THEN B[b] := a; A[a'] := A!a'+1; as := a' # tl as
       ELSE A[a] := A!a+1
       FI
  FI
 OD
 [wf A \<and> inj_on (match A) {<n} \<and> stable A {<n} \<and> opti\<^sub>a A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [as = [0..<n] \<and> A = replicate n 0 \<and> B = replicate n 0 \<and> M = replicate n False]
WHILE as \<noteq> [] INV {invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as}  VAR {var A ({<n} - set as)}
DO a := hd as; b := match A a; IF \<not> M ! b THEN M := M[b := True]; B := B[b := a]; as := tl as  ELSE a' := B ! b; IF P\<^sub>b ! match A a' \<turnstile> a < a' THEN B := B[b := a]; A := A[a' := A ! a' + 1]; as := a' # tl as  ELSE A := A[a := A ! a + 1] FI FI OD
[local.wf A \<and> inj_on (match A) {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A]
[PROOF STEP]
proof (vcg_tc, goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A B M a a' as b. as = [0..<n] \<and> A = replicate n 0 \<and> B = replicate n 0 \<and> M = replicate n False \<Longrightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as
 2. \<And>na A B M a a' as b. ((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)))
 3. \<And>A B M a a' as b. (invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> \<not> as \<noteq> [] \<Longrightarrow> local.wf A \<and> inj_on (match A) {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
as_ = [0..<n] \<and> A_ = replicate n 0 \<and> B_ = replicate n 0 \<and> M_ = replicate n False

goal (3 subgoals):
 1. \<And>A B M a a' as b. as = [0..<n] \<and> A = replicate n 0 \<and> B = replicate n 0 \<and> M = replicate n False \<Longrightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as
 2. \<And>na A B M a a' as b. ((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)))
 3. \<And>A B M a a' as b. (invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> \<not> as \<noteq> [] \<Longrightarrow> local.wf A \<and> inj_on (match A) {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
as_ = [0..<n] \<and> A_ = replicate n 0 \<and> B_ = replicate n 0 \<and> M_ = replicate n False

goal (1 subgoal):
 1. invAM A_ ({<n} - set as_) \<and> (length B_ = n \<and> length M_ = n \<and> {<n} - set as_ = (!) B_ ` _Collect b (b < n \<and> M_ ! b) \<and> (\<forall>b<n. M_ ! b \<longrightarrow> B_ ! b < n \<and> match A_ (B_ ! b) = b)) \<and> invas as_
[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_ ({<n} - set as_) \<and> (length B_ = n \<and> length M_ = n \<and> {<n} - set as_ = (!) B_ ` _Collect b (b < n \<and> M_ ! b) \<and> (\<forall>b<n. M_ ! b \<longrightarrow> B_ ! b < n \<and> match A_ (B_ ! b) = b)) \<and> invas as_

goal (2 subgoals):
 1. \<And>na A B M a a' as b. ((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)))
 2. \<And>A B M a a' as b. (invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> \<not> as \<noteq> [] \<Longrightarrow> local.wf A \<and> inj_on (match A) {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>na A B M a a' as b. ((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)))
 2. \<And>A B M a a' as b. (invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> \<not> as \<noteq> [] \<Longrightarrow> local.wf A \<and> inj_on (match A) {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
(invAM A_ ({<n} - set as_) \<and> (length B_ = n \<and> length M_ = n \<and> {<n} - set as_ = (!) B_ ` _Collect b (b < n \<and> M_ ! b) \<and> (\<forall>b<n. M_ ! b \<longrightarrow> B_ ! b < n \<and> match A_ (B_ ! b) = b)) \<and> invas as_) \<and> \<not> as_ \<noteq> []

goal (2 subgoals):
 1. \<And>na A B M a a' as b. ((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)))
 2. \<And>A B M a a' as b. (invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> \<not> as \<noteq> [] \<Longrightarrow> local.wf A \<and> inj_on (match A) {<n} \<and> local.stable A {<n} \<and> opti\<^sub>a A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(invAM A_ ({<n} - set as_) \<and> (length B_ = n \<and> length M_ = n \<and> {<n} - set as_ = (!) B_ ` _Collect b (b < n \<and> M_ ! b) \<and> (\<forall>b<n. M_ ! b \<longrightarrow> B_ ! b < n \<and> match A_ (B_ ! b) = b)) \<and> invas as_) \<and> \<not> as_ \<noteq> []

goal (1 subgoal):
 1. local.wf A_ \<and> inj_on (match 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_ ({<n} - set as_) \<and> (length B_ = n \<and> length M_ = n \<and> {<n} - set as_ = (!) B_ ` _Collect b (b < n \<and> M_ ! b) \<and> (\<forall>b<n. M_ ! b \<longrightarrow> B_ ! b < n \<and> match A_ (B_ ! b) = b)) \<and> invas as_) \<and> \<not> as_ \<noteq> []
\<lbrakk>matching ?A {<n}; pref_match ?A {<n}\<rbrakk> \<Longrightarrow> local.stable ?A {<n}

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

goal (1 subgoal):
 1. \<And>na A B M a a' as b. ((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na A B M a a' as b. ((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
case (2 v A B M _ a' as)
[PROOF STATE]
proof (state)
this:
((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = v

goal (1 subgoal):
 1. \<And>na A B M a a' as b. ((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
let ?M = "{<n} - set as"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na A B M a a' as b. ((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < 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 "opti\<^sub>a A" and notall: "as \<noteq> []" and v: "var A ?M = v"
    and as: "invas as" and invAB: "invAB' A B M ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((invAM A ({<n} - set as) &&& matching A ({<n} - set as)) &&& local.wf A &&& {<n} - set as \<subseteq> {<n} &&& pref_match A ({<n} - set as)) &&& (opti\<^sub>a A &&& as \<noteq> []) &&& var A ({<n} - set as) = v &&& invas as &&& length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = v

goal (1 subgoal):
 1. ((invAM A ({<n} - set as) &&& matching A ({<n} - set as)) &&& local.wf A &&& {<n} - set as \<subseteq> {<n} &&& pref_match A ({<n} - set as)) &&& (opti\<^sub>a A &&& as \<noteq> []) &&& var A ({<n} - set as) = v &&& invas as &&& length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invAM A ({<n} - set as)
matching A ({<n} - set as)
local.wf A
{<n} - set as \<subseteq> {<n}
pref_match A ({<n} - set as)
opti\<^sub>a A
as \<noteq> []
var A ({<n} - set as) = v
invas as
length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)

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

goal (1 subgoal):
 1. \<And>na A B M a a' as b. ((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < 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 ({<n} - set as)

goal (1 subgoal):
 1. \<forall>a<n. preferred A a \<subseteq> match A ` ({<n} - set as)
[PROOF STEP]
unfolding pref_match'_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a<n. \<forall>b\<in>preferred A a. \<exists>a'\<in>{<n} - set as. 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 ` ({<n} - set as)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>a<n. preferred A a \<subseteq> match A ` ({<n} - set as)

goal (1 subgoal):
 1. \<And>na A B M a a' as b. ((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
from notall
[PROOF STATE]
proof (chain)
picking this:
as \<noteq> []
[PROOF STEP]
obtain a as' where aseq: "as = a # as'"
[PROOF STATE]
proof (prove)
using this:
as \<noteq> []

goal (1 subgoal):
 1. (\<And>a as'. as = a # as' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce simp: neq_Nil_conv)
[PROOF STATE]
proof (state)
this:
as = a # as'

goal (1 subgoal):
 1. \<And>na A B M a a' as b. ((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
have set_as: "?M \<union> {a} = {<n} - set as'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<n} - set as \<union> {a} = {<n} - set as'
[PROOF STEP]
using as aseq
[PROOF STATE]
proof (prove)
using this:
invas as
as = a # as'

goal (1 subgoal):
 1. {<n} - set as \<union> {a} = {<n} - set as'
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{<n} - set as \<union> {a} = {<n} - set as'

goal (1 subgoal):
 1. \<And>na A B M a a' as b. ((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
have a: "a < n \<and> a \<notin> ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < n \<and> a \<notin> {<n} - set as
[PROOF STEP]
using as
[PROOF STATE]
proof (prove)
using this:
invas as

goal (1 subgoal):
 1. a < n \<and> a \<notin> {<n} - set as
[PROOF STEP]
unfolding aseq
[PROOF STATE]
proof (prove)
using this:
invas (a # as')

goal (1 subgoal):
 1. a < n \<and> a \<notin> {<n} - set (a # as')
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
a < n \<and> a \<notin> {<n} - set as

goal (1 subgoal):
 1. \<And>na A B M a a' as b. ((invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> as \<noteq> []) \<and> var A ({<n} - set as) = na \<Longrightarrow> (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < na)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)))
[PROOF STEP]
proof (simp only: aseq list.sel, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], a, a', as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], a, a', as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)))
[PROOF STEP]
show ?case (is "(?not_matched \<longrightarrow> ?THEN) \<and> (\<not> ?not_matched \<longrightarrow> ?ELSE)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> M ! match A a \<longrightarrow> (A, B[match A a := a], M[match A a := True], a, a', as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> \<not> M ! match A a \<longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)))
[PROOF STEP]
proof (rule; rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], a, a', as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)
 2. \<not> \<not> M ! match A a \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
assume ?not_matched
[PROOF STATE]
proof (state)
this:
\<not> M ! match A a

goal (2 subgoals):
 1. \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], a, a', as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)
 2. \<not> \<not> M ! match A a \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> M ! match A a
[PROOF STEP]
have nm: "match A a \<notin> match A ` ?M"
[PROOF STATE]
proof (prove)
using this:
\<not> M ! match A a

goal (1 subgoal):
 1. match A a \<notin> match A ` ({<n} - set as)
[PROOF STEP]
using invAB set_as
[PROOF STATE]
proof (prove)
using this:
\<not> M ! match A a
length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)
{<n} - set as \<union> {a} = {<n} - set as'

goal (1 subgoal):
 1. match A a \<notin> match A ` ({<n} - set as)
[PROOF STEP]
unfolding aseq
[PROOF STATE]
proof (prove)
using this:
\<not> M ! match A a
length B = n \<and> length M = n \<and> {<n} - set (a # as') = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)
{<n} - set (a # as') \<union> {a} = {<n} - set as'

goal (1 subgoal):
 1. match A a \<notin> match A ` ({<n} - set (a # as'))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
match A a \<notin> match A ` ({<n} - set as)

goal (2 subgoals):
 1. \<not> M ! match A a \<Longrightarrow> (A, B[match A a := a], M[match A a := True], a, a', as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)
 2. \<not> \<not> M ! match A a \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
show ?THEN
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A, B[match A a := a], M[match A a := True], a, a', as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < 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 ({<n} - set as') \<and> (length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n \<and> {<n} - set as' = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M[match A a := True] ! b) \<and> (\<forall>b<n. M[match A a := True] ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match A (B[match A a := a] ! b) = b)) \<and> invas as'
 2. var A ({<n} - set as') < v
[PROOF STEP]
have invAM': "invAM A ({<n} - set as')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM A ({<n} - set as')
[PROOF STEP]
using invAM_match[OF invAM a nm]
[PROOF STATE]
proof (prove)
using this:
invAM A ({<n} - set as \<union> {a})

goal (1 subgoal):
 1. invAM A ({<n} - set as')
[PROOF STEP]
unfolding set_as[symmetric]
[PROOF STATE]
proof (prove)
using this:
invAM A ({<n} - set as \<union> {a})

goal (1 subgoal):
 1. invAM A ({<n} - set as \<union> {a})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
invAM A ({<n} - set as')

goal (2 subgoals):
 1. invAM A ({<n} - set as') \<and> (length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n \<and> {<n} - set as' = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M[match A a := True] ! b) \<and> (\<forall>b<n. M[match A a := True] ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match A (B[match A a := a] ! b) = b)) \<and> invas as'
 2. var A ({<n} - set as') < v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invAM A ({<n} - set as')
[PROOF STEP]
have invAB': "invAB' A (B[match A a := a]) (M[match A a := True]) ({<n} - set as')"
[PROOF STATE]
proof (prove)
using this:
invAM A ({<n} - set as')

goal (1 subgoal):
 1. length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n \<and> {<n} - set as' = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M[match A a := True] ! b) \<and> (\<forall>b<n. M[match A a := True] ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match A (B[match A a := a] ! b) = b)
[PROOF STEP]
using invAB \<open>?not_matched\<close> set_as match_less_n[OF A] a
[PROOF STATE]
proof (prove)
using this:
invAM A ({<n} - set as')
length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)
\<not> M ! match A a
{<n} - set as \<union> {a} = {<n} - set as'
?a < n \<Longrightarrow> match A ?a < n
a < n \<and> a \<notin> {<n} - set as

goal (1 subgoal):
 1. length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n \<and> {<n} - set as' = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M[match A a := True] ! b) \<and> (\<forall>b<n. M[match A a := True] ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match A (B[match A a := a] ! b) = b)
[PROOF STEP]
by (auto simp add: image_def nth_list_update)
[PROOF STATE]
proof (state)
this:
length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n \<and> {<n} - set as' = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M[match A a := True] ! b) \<and> (\<forall>b<n. M[match A a := True] ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match A (B[match A a := a] ! b) = b)

goal (2 subgoals):
 1. invAM A ({<n} - set as') \<and> (length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n \<and> {<n} - set as' = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M[match A a := True] ! b) \<and> (\<forall>b<n. M[match A a := True] ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match A (B[match A a := a] ! b) = b)) \<and> invas as'
 2. var A ({<n} - set as') < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invAM A ({<n} - set as') \<and> (length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n \<and> {<n} - set as' = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M[match A a := True] ! b) \<and> (\<forall>b<n. M[match A a := True] ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match A (B[match A a := a] ! b) = b)) \<and> invas as'
 2. var A ({<n} - set as') < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM A ({<n} - set as') \<and> (length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n \<and> {<n} - set as' = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M[match A a := True] ! b) \<and> (\<forall>b<n. M[match A a := True] ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match A (B[match A a := a] ! b) = b)) \<and> invas as'
[PROOF STEP]
using invAM' invAB as invAB'
[PROOF STATE]
proof (prove)
using this:
invAM A ({<n} - set as')
length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)
invas as
length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n \<and> {<n} - set as' = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M[match A a := True] ! b) \<and> (\<forall>b<n. M[match A a := True] ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match A (B[match A a := a] ! b) = b)

goal (1 subgoal):
 1. invAM A ({<n} - set as') \<and> (length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n \<and> {<n} - set as' = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M[match A a := True] ! b) \<and> (\<forall>b<n. M[match A a := True] ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match A (B[match A a := a] ! b) = b)) \<and> invas as'
[PROOF STEP]
unfolding set_as aseq
[PROOF STATE]
proof (prove)
using this:
invAM A ({<n} - set as')
length B = n \<and> length M = n \<and> {<n} - set (a # as') = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)
invas (a # as')
length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n \<and> {<n} - set as' = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M[match A a := True] ! b) \<and> (\<forall>b<n. M[match A a := True] ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match A (B[match A a := a] ! b) = b)

goal (1 subgoal):
 1. invAM A ({<n} - set as') \<and> (length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n \<and> {<n} - set as' = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M[match A a := True] ! b) \<and> (\<forall>b<n. M[match A a := True] ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match A (B[match A a := a] ! b) = b)) \<and> invas as'
[PROOF STEP]
by (metis distinct.simps(2) insert_subset list.simps(15))
[PROOF STATE]
proof (state)
this:
invAM A ({<n} - set as') \<and> (length (B[match A a := a]) = n \<and> length (M[match A a := True]) = n \<and> {<n} - set as' = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M[match A a := True] ! b) \<and> (\<forall>b<n. M[match A a := True] ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match A (B[match A a := a] ! b) = b)) \<and> invas as'

goal (1 subgoal):
 1. var A ({<n} - set as') < v
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. var A ({<n} - set as') < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var A ({<n} - set as') < v
[PROOF STEP]
using var_match[OF m M _ pref_match1, of a] a atLeast0LessThan
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{<n} - set as \<noteq> {<n}; a \<notin> {<n} - set as\<rbrakk> \<Longrightarrow> var A ({<n} - set as \<union> {a}) < var A ({<n} - set as)
a < n \<and> a \<notin> {<n} - set as
{<?n} = {..<?n}

goal (1 subgoal):
 1. var A ({<n} - set as') < v
[PROOF STEP]
unfolding set_as v
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{<n} - set as \<noteq> {<n}; a \<notin> {<n} - set as\<rbrakk> \<Longrightarrow> var A ({<n} - set as') < v
a < n \<and> a \<notin> {<n} - set as
{<?n} = {..<?n}

goal (1 subgoal):
 1. var A ({<n} - set as') < v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
var A ({<n} - set as') < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(A, B[match A a := a], M[match A a := True], a, a', as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)

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

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

goal (1 subgoal):
 1. match A a \<in> match A ` ({<n} - ({a} \<union> set as'))
[PROOF STEP]
using  match_less_n[OF A] a invAB
[PROOF STATE]
proof (prove)
using this:
\<not> \<not> M ! match A a
?a < n \<Longrightarrow> match A ?a < n
a < n \<and> a \<notin> {<n} - set as
length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)

goal (1 subgoal):
 1. match A a \<in> match A ` ({<n} - ({a} \<union> set as'))
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>M ! match A a; \<And>a. a < length B \<Longrightarrow> match A a < length B; a < length B; a \<notin> (!) B ` _Collect b (b < length B \<and> M ! b); n = length B; length M = length B; {<length B} - set as = (!) B ` _Collect b (b < length B \<and> M ! b); \<forall>b<length B. M ! b \<longrightarrow> B ! b < length B \<and> match A (B ! b) = b\<rbrakk> \<Longrightarrow> match A a \<in> match A ` ({<length B} - ({a} \<union> set as'))
[PROOF STEP]
by (metis (lifting) image_eqI list.simps(15) mem_Collect_eq aseq)
[PROOF STATE]
proof (state)
this:
match A a \<in> match A ` ({<n} - ({a} \<union> set as'))

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

goal (1 subgoal):
 1. Suc (A ! a) < n
[PROOF STEP]
using more_choices[OF m M, of a] a pref_match1
[PROOF STATE]
proof (prove)
using this:
match A a \<in> match A ` ({<n} - ({a} \<union> set as'))
\<lbrakk>{<n} - set as \<noteq> {<n}; preferred A a \<subseteq> match A ` ({<n} - set as); a < n; match A a \<in> match A ` ({<n} - set as)\<rbrakk> \<Longrightarrow> A ! a + 1 < n
a < n \<and> a \<notin> {<n} - set as
\<forall>a<n. preferred A a \<subseteq> match A ` ({<n} - set as)

goal (1 subgoal):
 1. Suc (A ! a) < n
[PROOF STEP]
using aseq atLeast0LessThan
[PROOF STATE]
proof (prove)
using this:
match A a \<in> match A ` ({<n} - ({a} \<union> set as'))
\<lbrakk>{<n} - set as \<noteq> {<n}; preferred A a \<subseteq> match A ` ({<n} - set as); a < n; match A a \<in> match A ` ({<n} - set as)\<rbrakk> \<Longrightarrow> A ! a + 1 < n
a < n \<and> a \<notin> {<n} - set as
\<forall>a<n. preferred A a \<subseteq> match A ` ({<n} - set as)
as = a # as'
{<?n} = {..<?n}

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

goal (1 subgoal):
 1. \<not> \<not> M ! match A a \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
let ?a = "B ! match A a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<not> M ! match A a \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
have a': "?a \<in> ?M \<and> match A ?a = match A a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B ! match A a \<in> {<n} - set as \<and> match A (B ! match A a) = match A a
[PROOF STEP]
using invAB match_less_n[OF A] matched a
[PROOF STATE]
proof (prove)
using this:
length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)
?a < n \<Longrightarrow> match A ?a < n
\<not> \<not> M ! match A a
a < n \<and> a \<notin> {<n} - set as

goal (1 subgoal):
 1. B ! match A a \<in> {<n} - set as \<and> match A (B ! match A a) = match A a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B ! match A a \<in> {<n} - set as \<and> match A (B ! match A a) = match A a

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

goal (1 subgoal):
 1. B ! match A a < n &&& a \<noteq> B ! match A a
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
B ! match A a \<in> {<n} - set as \<and> match A (B ! match A a) = match A a
a < n \<and> a \<notin> {<n} - set as

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

goal (1 subgoal):
 1. \<not> \<not> M ! match A a \<Longrightarrow> (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
show ?ELSE
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
unfolding aseq option.sel
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
proof (goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

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

goal (2 subgoals):
 1. P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)
 2. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)
[PROOF STEP]
show ?THEN
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < 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[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) \<and> (length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)) \<and> invas (B ! match A a # as')
 2. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) < v
[PROOF STEP]
have *: "{<n} - set as - {?a} \<union> {a} = {<n} - set (?a # as')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {<n} - set as - {B ! match A a} \<union> {a} = {<n} - set (B ! match A a # as')
[PROOF STEP]
using a a' as aseq
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> {<n} - set as
B ! match A a \<in> {<n} - set as \<and> match A (B ! match A a) = match A a
invas as
as = a # as'

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

goal (2 subgoals):
 1. invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) \<and> (length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)) \<and> invas (B ! match A a # as')
 2. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) < v
[PROOF STEP]
have a'neq: "\<forall>b<n. b \<noteq> match A a \<longrightarrow> M!b \<longrightarrow> ?a \<noteq> B!b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b<n. b \<noteq> match A a \<longrightarrow> M ! b \<longrightarrow> B ! match A a \<noteq> B ! b
[PROOF STEP]
using invAB a'
[PROOF STATE]
proof (prove)
using this:
length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)
B ! match A a \<in> {<n} - set as \<and> match A (B ! match A a) = match A a

goal (1 subgoal):
 1. \<forall>b<n. b \<noteq> match A a \<longrightarrow> M ! b \<longrightarrow> B ! match A a \<noteq> B ! b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>b<n. b \<noteq> match A a \<longrightarrow> M ! b \<longrightarrow> B ! match A a \<noteq> B ! b

goal (2 subgoals):
 1. invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) \<and> (length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)) \<and> invas (B ! match A a # as')
 2. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) < v
[PROOF STEP]
have invAB': "invAB' (A[?a := A ! ?a + 1]) (B[match A a := a]) M ({<n} - set (?a#as'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)
[PROOF STEP]
using invAB aseq * \<open>a \<noteq> ?a\<close> a' match_less_n[OF A, of a] a
[PROOF STATE]
proof (prove)
using this:
length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)
as = a # as'
{<n} - set as - {B ! match A a} \<union> {a} = {<n} - set (B ! match A a # as')
a \<noteq> B ! match A a
B ! match A a \<in> {<n} - set as \<and> match A (B ! match A a) = match A a
a < n \<Longrightarrow> match A a < n
a < n \<and> a \<notin> {<n} - set as

goal (1 subgoal):
 1. length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)
[PROOF STEP]
apply (simp add: nth_list_update)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length B = n \<and> length M = n \<and> {<n} - ({a} \<union> set as') = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b); as = a # as'; {a} \<union> ((!) B ` _Collect b (b < n \<and> M ! b) - {B ! match A a}) = {<n} - ({B ! match A a} \<union> set as'); a \<noteq> B ! match A a; B ! match A a \<in> (!) B ` _Collect b (b < n \<and> M ! b) \<and> match A (B ! match A a) = match A a; match A a < n; a < n \<and> a \<notin> (!) B ` _Collect b (b < n \<and> M ! b)\<rbrakk> \<Longrightarrow> {<n} - ({B ! match A a} \<union> set as') = (\<lambda>a. a) ` (_Collect b (b < n \<and> M ! b) \<inter> {match A a}) \<union> (!) B ` (_Collect b (b < n \<and> M ! b) \<inter> _Collect x (match A a \<noteq> x)) \<and> (\<forall>b. (match A a = b \<longrightarrow> M ! b \<longrightarrow> match (A[B ! b := Suc (A ! (B ! b))]) a = b) \<and> (match A a \<noteq> b \<longrightarrow> b < n \<longrightarrow> M ! b \<longrightarrow> match (A[B ! match A a := Suc (A ! (B ! match A a))]) (B ! b) = b))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length B = n \<and> length M = n \<and> {<n} - ({a} \<union> set as') = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b); as = a # as'; {a} \<union> ((!) B ` _Collect b (b < n \<and> M ! b) - {B ! match A a}) = {<n} - ({B ! match A a} \<union> set as'); a \<noteq> B ! match A a; B ! match A a \<in> (!) B ` _Collect b (b < n \<and> M ! b) \<and> match A (B ! match A a) = match A a; match A a < n; a < n \<and> a \<notin> (!) B ` _Collect b (b < n \<and> M ! b)\<rbrakk> \<Longrightarrow> {<n} - ({B ! match A a} \<union> set as') = (\<lambda>a. a) ` (_Collect b (b < n \<and> M ! b) \<inter> {match A a}) \<union> (!) B ` (_Collect b (b < n \<and> M ! b) \<inter> _Collect x (match A a \<noteq> x))
 2. \<lbrakk>length B = n \<and> length M = n \<and> {<n} - ({a} \<union> set as') = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b); as = a # as'; {a} \<union> ((!) B ` _Collect b (b < n \<and> M ! b) - {B ! match A a}) = {<n} - ({B ! match A a} \<union> set as'); a \<noteq> B ! match A a; B ! match A a \<in> (!) B ` _Collect b (b < n \<and> M ! b) \<and> match A (B ! match A a) = match A a; match A a < n; a < n \<and> a \<notin> (!) B ` _Collect b (b < n \<and> M ! b)\<rbrakk> \<Longrightarrow> \<forall>b. (match A a = b \<longrightarrow> M ! b \<longrightarrow> match (A[B ! b := Suc (A ! (B ! b))]) a = b) \<and> (match A a \<noteq> b \<longrightarrow> b < n \<longrightarrow> M ! b \<longrightarrow> match (A[B ! match A a := Suc (A ! (B ! match A a))]) (B ! b) = b)
[PROOF STEP]
apply(auto simp add:  image_def)[]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length B = n \<and> length M = n \<and> {<n} - ({a} \<union> set as') = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b); as = a # as'; {a} \<union> ((!) B ` _Collect b (b < n \<and> M ! b) - {B ! match A a}) = {<n} - ({B ! match A a} \<union> set as'); a \<noteq> B ! match A a; B ! match A a \<in> (!) B ` _Collect b (b < n \<and> M ! b) \<and> match A (B ! match A a) = match A a; match A a < n; a < n \<and> a \<notin> (!) B ` _Collect b (b < n \<and> M ! b)\<rbrakk> \<Longrightarrow> \<forall>b. (match A a = b \<longrightarrow> M ! b \<longrightarrow> match (A[B ! b := Suc (A ! (B ! b))]) a = b) \<and> (match A a \<noteq> b \<longrightarrow> b < n \<longrightarrow> M ! b \<longrightarrow> match (A[B ! match A a := Suc (A ! (B ! match A a))]) (B ! b) = b)
[PROOF STEP]
apply (clarsimp simp add: match_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>as = a # as'; {a} \<union> ((!) B ` _Collect b (b < length B \<and> M ! b) - {B ! (P\<^sub>a ! a ! (A ! a))}) = {<length B} - ({B ! (P\<^sub>a ! a ! (A ! a))} \<union> set as'); a \<noteq> B ! (P\<^sub>a ! a ! (A ! a)); P\<^sub>a ! a ! (A ! a) < length B; n = length B; a < length B; a \<notin> (!) B ` _Collect b (b < length B \<and> M ! b); length M = length B; M ! (P\<^sub>a ! a ! (A ! a)); {<length B} - ({a} \<union> set as') = (!) B ` _Collect b (b < length B \<and> M ! b); \<forall>b<length B. M ! b \<longrightarrow> B ! b < length B \<and> P\<^sub>a ! (B ! b) ! (A ! (B ! b)) = b\<rbrakk> \<Longrightarrow> (P\<^sub>a ! a ! (A ! a) = b \<longrightarrow> M ! b \<longrightarrow> P\<^sub>a ! a ! (A[B ! b := Suc (A ! (B ! b))] ! a) = b) \<and> (P\<^sub>a ! a ! (A ! a) \<noteq> b \<longrightarrow> b < length B \<longrightarrow> M ! b \<longrightarrow> P\<^sub>a ! (B ! b) ! (A[B ! (P\<^sub>a ! a ! (A ! a)) := Suc (A ! (B ! (P\<^sub>a ! a ! (A ! a))))] ! (B ! b)) = b)
[PROOF STEP]
apply (metis (opaque_lifting) nth_list_update_neq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)

goal (2 subgoals):
 1. invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) \<and> (length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)) \<and> invas (B ! match A a # as')
 2. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) \<and> (length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)) \<and> invas (B ! match A a # as')
 2. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) \<and> (length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)) \<and> invas (B ! match A a # as')
[PROOF STEP]
using invAM_swap[OF invAM a a' \<open>?pref\<close>] invAB'
[PROOF STATE]
proof (prove)
using this:
invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set as - {B ! match A a} \<union> {a})
length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)

goal (1 subgoal):
 1. invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) \<and> (length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)) \<and> invas (B ! match A a # as')
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as'))
length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)

goal (1 subgoal):
 1. invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) \<and> (length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)) \<and> invas (B ! match A a # as')
[PROOF STEP]
using a' as aseq
[PROOF STATE]
proof (prove)
using this:
invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as'))
length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)
B ! match A a \<in> {<n} - set as \<and> match A (B ! match A a) = match A a
invas as
as = a # as'

goal (1 subgoal):
 1. invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) \<and> (length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)) \<and> invas (B ! match A a # as')
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
invAM (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) \<and> (length (B[match A a := a]) = n \<and> length M = n \<and> {<n} - set (B ! match A a # as') = (!) (B[match A a := a]) ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B[match A a := a] ! b < n \<and> match (A[B ! match A a := A ! (B ! match A a) + 1]) (B[match A a := a] ! b) = b)) \<and> invas (B ! match A a # as')

goal (1 subgoal):
 1. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) < v
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) < v
[PROOF STEP]
have "card({<n} - set as) = card({<n} - set (?a # as'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({<n} - set as) = card ({<n} - set (B ! match A a # as'))
[PROOF STEP]
using a a' as aseq
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> {<n} - set as
B ! match A a \<in> {<n} - set as \<and> match A (B ! match A a) = match A a
invas as
as = a # as'

goal (1 subgoal):
 1. card ({<n} - set as) = card ({<n} - set (B ! match A a # as'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card ({<n} - set as) = card ({<n} - set (B ! match A a # as'))

goal (1 subgoal):
 1. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) < v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
card ({<n} - set as) = card ({<n} - set (B ! match A a # as'))

goal (1 subgoal):
 1. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) < v
[PROOF STEP]
using v var_next[OF m M _ pref_match1, of ?a] \<open>?a < n\<close> a atLeast0LessThan
[PROOF STATE]
proof (prove)
using this:
card ({<n} - set as) = card ({<n} - set (B ! match A a # as'))
var A ({<n} - set as) = v
\<lbrakk>{<n} - set as \<noteq> {<n}; B ! match A a < n\<rbrakk> \<Longrightarrow> var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set as) < var A ({<n} - set as)
B ! match A a < n
a < n \<and> a \<notin> {<n} - set as
{<?n} = {..<?n}

goal (1 subgoal):
 1. var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) < v
[PROOF STEP]
by (metis Suc_eq_plus1 lessThan_iff var_def)
[PROOF STATE]
proof (state)
this:
var (A[B ! match A a := A ! (B ! match A a) + 1]) ({<n} - set (B ! match A a # as')) < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(A[B ! match A a := A ! (B ! match A a) + 1], B[match A a := a], M, a, B ! match A a, B ! match A a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)

goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)
[PROOF STEP]
assume "\<not> ?pref"
[PROOF STATE]
proof (state)
this:
\<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a

goal (1 subgoal):
 1. \<not> P\<^sub>b ! match A (B ! match A a) \<turnstile> a < B ! match A a \<Longrightarrow> (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)
[PROOF STEP]
show ?ELSE
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < 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]) ({<n} - set (a # as')) \<and> (length B = n \<and> length M = n \<and> {<n} - set (a # as') = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match (A[a := A ! a + 1]) (B ! b) = b)) \<and> invas (a # as')
 2. var (A[a := A ! a + 1]) ({<n} - set (a # as')) < v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. invAM (A[a := A ! a + 1]) ({<n} - set (a # as')) \<and> (length B = n \<and> length M = n \<and> {<n} - set (a # as') = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match (A[a := A ! a + 1]) (B ! b) = b)) \<and> invas (a # as')
 2. var (A[a := A ! a + 1]) ({<n} - set (a # as')) < v
[PROOF STEP]
have "invAB' (A[a := A ! a + 1]) B M ({<n} - set as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match (A[a := A ! a + 1]) (B ! b) = b)
[PROOF STEP]
using invAB a \<open>a \<noteq> ?a\<close>
[PROOF STATE]
proof (prove)
using this:
length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)
a < n \<and> a \<notin> {<n} - set as
a \<noteq> B ! match A a

goal (1 subgoal):
 1. length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match (A[a := A ! a + 1]) (B ! b) = b)
[PROOF STEP]
by (metis match_def nth_list_update_neq)
[PROOF STATE]
proof (state)
this:
length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match (A[a := A ! a + 1]) (B ! b) = b)

goal (2 subgoals):
 1. invAM (A[a := A ! a + 1]) ({<n} - set (a # as')) \<and> (length B = n \<and> length M = n \<and> {<n} - set (a # as') = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match (A[a := A ! a + 1]) (B ! b) = b)) \<and> invas (a # as')
 2. var (A[a := A ! a + 1]) ({<n} - set (a # as')) < v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match (A[a := A ! a + 1]) (B ! b) = b)

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) ({<n} - set (a # as')) \<and> (length B = n \<and> length M = n \<and> {<n} - set (a # as') = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match (A[a := A ! a + 1]) (B ! b) = b)) \<and> invas (a # as')
[PROOF STEP]
using invAM_next[OF invAM a a' \<open>\<not> ?pref\<close>] as aseq
[PROOF STATE]
proof (prove)
using this:
length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match (A[a := A ! a + 1]) (B ! b) = b)
invAM (A[a := A ! a + 1]) ({<n} - set as)
invas as
as = a # as'

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) ({<n} - set (a # as')) \<and> (length B = n \<and> length M = n \<and> {<n} - set (a # as') = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match (A[a := A ! a + 1]) (B ! b) = b)) \<and> invas (a # as')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
invAM (A[a := A ! a + 1]) ({<n} - set (a # as')) \<and> (length B = n \<and> length M = n \<and> {<n} - set (a # as') = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match (A[a := A ! a + 1]) (B ! b) = b)) \<and> invas (a # as')

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

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) ({<n} - set (a # as')) < v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var (A[a := A ! a + 1]) ({<n} - set (a # as')) < v
[PROOF STEP]
using a v var_next[OF m M _ pref_match1, of a] aseq
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> {<n} - set as
var A ({<n} - set as) = v
\<lbrakk>{<n} - set as \<noteq> {<n}; a < n\<rbrakk> \<Longrightarrow> var (A[a := A ! a + 1]) ({<n} - set as) < var A ({<n} - set as)
as = a # as'

goal (1 subgoal):
 1. var (A[a := A ! a + 1]) ({<n} - set (a # as')) < v
[PROOF STEP]
by (metis Suc_eq_plus1 atLeast0LessThan lessThan_iff)
[PROOF STATE]
proof (state)
this:
var (A[a := A ! a + 1]) ({<n} - set (a # as')) < v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(A[a := A ! a + 1], B, M, a, B ! match A a, a # as', match A a) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<not> M ! match A (hd as) \<longrightarrow> (A, B[match A (hd as) := hd as], M[match A (hd as) := True], hd as, a', tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> \<not> M ! match A (hd as) \<longrightarrow> (P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[B ! match A (hd as) := A ! (B ! match A (hd as)) + 1], B[match A (hd as) := hd as], M, hd as, B ! match A (hd as), B ! match A (hd as) # tl as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)) \<and> (\<not> P\<^sub>b ! match A (B ! match A (hd as)) \<turnstile> hd as < B ! match A (hd as) \<longrightarrow> (A[hd as := A ! hd as + 1], B, M, hd as, B ! match A (hd as), as, match A (hd as)) \<in> _Collect s ((case s of (A, B, M, a, a', as, b) \<Rightarrow> invAM A ({<n} - set as) \<and> (length B = n \<and> length M = n \<and> {<n} - set as = (!) B ` _Collect b (b < n \<and> M ! b) \<and> (\<forall>b<n. M ! b \<longrightarrow> B ! b < n \<and> match A (B ! b) = b)) \<and> invas as) \<and> (case s of (A, B, M, a, a', as, b) \<Rightarrow> var A ({<n} - set as)) < v)))

goal:
No subgoals!
[PROOF STEP]
qed