[STATEMENT]
lemma pref_match'_iff: "wf A \<Longrightarrow> pref_match' A M = pref_match A M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.wf A \<Longrightarrow> pref_match' A M = pref_match A M
[PROOF STEP]
apply (auto simp add: pref_match'_def pref_match_def imp_ex prefers_def match_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>set A \<subseteq> {<length A}; n = length A; \<forall>a<length A. \<forall>b\<in>{<A ! a}. \<exists>a'\<in>M. P\<^sub>a ! a ! b = P\<^sub>a ! a' ! (A ! a') \<and> index (P\<^sub>b ! (P\<^sub>a ! a ! b)) a' < index (P\<^sub>b ! (P\<^sub>a ! a ! b)) a; a < length A; b < length A; index (P\<^sub>a ! a) b < index (P\<^sub>a ! a) (P\<^sub>a ! a ! (A ! a))\<rbrakk> \<Longrightarrow> \<exists>a'\<in>M. b = P\<^sub>a ! a' ! (A ! a') \<and> index (P\<^sub>b ! b) a' < index (P\<^sub>b ! b) a
 2. \<And>a b. \<lbrakk>set A \<subseteq> {<length A}; n = length A; \<forall>a<length A. \<forall>b<length A. index (P\<^sub>a ! a) b < index (P\<^sub>a ! a) (P\<^sub>a ! a ! (A ! a)) \<longrightarrow> (\<exists>a'\<in>M. b = P\<^sub>a ! a' ! (A ! a') \<and> index (P\<^sub>b ! b) a' < index (P\<^sub>b ! b) a); a < length A; b < A ! a\<rbrakk> \<Longrightarrow> \<exists>a'\<in>M. P\<^sub>a ! a ! b = P\<^sub>a ! a' ! (A ! a') \<and> index (P\<^sub>b ! (P\<^sub>a ! a ! b)) a' < index (P\<^sub>b ! (P\<^sub>a ! a ! b)) a
[PROOF STEP]
apply (smt (verit) P\<^sub>a_set atLeast0LessThan order.strict_trans index_first lessThan_iff linorder_neqE_nat nth_index)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>set A \<subseteq> {<length A}; n = length A; \<forall>a<length A. \<forall>b<length A. index (P\<^sub>a ! a) b < index (P\<^sub>a ! a) (P\<^sub>a ! a ! (A ! a)) \<longrightarrow> (\<exists>a'\<in>M. b = P\<^sub>a ! a' ! (A ! a') \<and> index (P\<^sub>b ! b) a' < index (P\<^sub>b ! b) a); a < length A; b < A ! a\<rbrakk> \<Longrightarrow> \<exists>a'\<in>M. P\<^sub>a ! a ! b = P\<^sub>a ! a' ! (A ! a') \<and> index (P\<^sub>b ! (P\<^sub>a ! a ! b)) a' < index (P\<^sub>b ! (P\<^sub>a ! a ! b)) a
[PROOF STEP]
by (smt (verit, best) P\<^sub>a_set atLeast0LessThan card_atLeastLessThan card_distinct diff_zero in_mono index_nth_id lessThan_iff less_trans nth_mem)


[STATEMENT]
lemma opti\<^sub>a_pessi\<^sub>b: assumes "opti\<^sub>a A" shows "pessi\<^sub>b A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pessi\<^sub>b A
[PROOF STEP]
unfolding pessi\<^sub>b_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>A'. matching A' {<n} \<and> local.stable A' {<n} \<and> (\<exists>a<n. \<exists>a'<n. match A a = match A' a' \<and> P\<^sub>b ! match A a \<turnstile> a < a')
[PROOF STEP]
proof (safe, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A' a a'. \<lbrakk>matching A' {<n}; local.stable A' {<n}; a < n; a' < n; match A a = match A' a'; P\<^sub>b ! match A a \<turnstile> a < a'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (1 A' a a')
[PROOF STATE]
proof (state)
this:
matching A' {<n}
local.stable A' {<n}
a < n
a' < n
match A a = match A' a'
P\<^sub>b ! match A a \<turnstile> a < a'

goal (1 subgoal):
 1. \<And>A' a a'. \<lbrakk>matching A' {<n}; local.stable A' {<n}; a < n; a' < n; match A a = match A' a'; P\<^sub>b ! match A a \<turnstile> a < a'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<not> P\<^sub>a!a \<turnstile>  match A a <  match A' a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> P\<^sub>a ! a \<turnstile> match A a < match A' a
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
matching A' {<n}
local.stable A' {<n}
a < n
a' < n
match A a = match A' a'
P\<^sub>b ! match A a \<turnstile> a < a'

goal (1 subgoal):
 1. \<not> P\<^sub>a ! a \<turnstile> match A a < match A' a
[PROOF STEP]
by (metis atLeast0LessThan blocks_def lessThan_iff prefers_asym stable_def)
[PROOF STATE]
proof (state)
this:
\<not> P\<^sub>a ! a \<turnstile> match A a < match A' a

goal (1 subgoal):
 1. \<And>A' a a'. \<lbrakk>matching A' {<n}; local.stable A' {<n}; a < n; a' < n; match A a = match A' a'; P\<^sub>b ! match A a \<turnstile> a < a'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with 1 \<open>opti\<^sub>a A\<close>
[PROOF STATE]
proof (chain)
picking this:
matching A' {<n}
local.stable A' {<n}
a < n
a' < n
match A a = match A' a'
P\<^sub>b ! match A a \<turnstile> a < a'
opti\<^sub>a A
\<not> P\<^sub>a ! a \<turnstile> match A a < match A' a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
matching A' {<n}
local.stable A' {<n}
a < n
a' < n
match A a = match A' a'
P\<^sub>b ! match A a \<turnstile> a < a'
opti\<^sub>a A
\<not> P\<^sub>a ! a \<turnstile> match A a < match A' a

goal (1 subgoal):
 1. False
[PROOF STEP]
using P\<^sub>a_set match_less_n opti\<^sub>a_def prefers_def
[PROOF STATE]
proof (prove)
using this:
matching A' {<n}
local.stable A' {<n}
a < n
a' < n
match A a = match A' a'
P\<^sub>b ! match A a \<turnstile> a < a'
opti\<^sub>a A
\<not> P\<^sub>a ! a \<turnstile> match A a < match A' a
?a < n \<Longrightarrow> length (P\<^sub>a ! ?a) = n \<and> set (P\<^sub>a ! ?a) = {<n}
\<lbrakk>local.wf ?A; ?a < n\<rbrakk> \<Longrightarrow> match ?A ?a < n
opti\<^sub>a ?A = (\<nexists>A'. matching A' {<n} \<and> local.stable A' {<n} \<and> (\<exists>a<n. P\<^sub>a ! a \<turnstile> match A' a < match ?A a))
(?P \<turnstile> ?x < ?y) = (index ?P ?x < index ?P ?y)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding matching_def
[PROOF STATE]
proof (prove)
using this:
local.wf A' \<and> inj_on (match A') {<n}
local.stable A' {<n}
a < n
a' < n
match A a = match A' a'
P\<^sub>b ! match A a \<turnstile> a < a'
opti\<^sub>a A
\<not> P\<^sub>a ! a \<turnstile> match A a < match A' a
?a < n \<Longrightarrow> length (P\<^sub>a ! ?a) = n \<and> set (P\<^sub>a ! ?a) = {<n}
\<lbrakk>local.wf ?A; ?a < n\<rbrakk> \<Longrightarrow> match ?A ?a < n
opti\<^sub>a ?A = (\<nexists>A'. (local.wf A' \<and> inj_on (match A') {<n}) \<and> local.stable A' {<n} \<and> (\<exists>a<n. P\<^sub>a ! a \<turnstile> match A' a < match ?A a))
(?P \<turnstile> ?x < ?y) = (index ?P ?x < index ?P ?y)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis (no_types) atLeast0LessThan inj_on_contraD lessThan_iff less_not_refl linorder_neqE_nat nth_index)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma opti\<^sub>a_inv:
assumes A: "wf A" and a: "a < n" and a': "a' < n" and same_match: "match A a' = match A a"
and pref: "P\<^sub>b ! match A a' \<turnstile> a' < a" and "opti\<^sub>a A"
shows "opti\<^sub>a (A[a := A ! a + 1])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. opti\<^sub>a (A[a := A ! a + 1])
[PROOF STEP]
proof (unfold opti\<^sub>a_def matching_def, rule notI, elim exE conjE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A' aa. \<lbrakk>inj_on (match A') {<n}; local.stable A' {<n}; length A' = n; set A' \<subseteq> {<n}; aa < n; P\<^sub>a ! aa \<turnstile> match A' aa < match (A[a := A ! a + 1]) aa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
note opti\<^sub>a = \<open>opti\<^sub>a A\<close>[unfolded opti\<^sub>a_def matching_def]
[PROOF STATE]
proof (state)
this:
\<nexists>A'. (local.wf A' \<and> inj_on (match A') {<n}) \<and> local.stable A' {<n} \<and> (\<exists>a<n. P\<^sub>a ! a \<turnstile> match A' a < match A a)

goal (1 subgoal):
 1. \<And>A' aa. \<lbrakk>inj_on (match A') {<n}; local.stable A' {<n}; length A' = n; set A' \<subseteq> {<n}; aa < n; P\<^sub>a ! aa \<turnstile> match A' aa < match (A[a := A ! a + 1]) aa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
let ?A = "A[a := A ! a + 1]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A' aa. \<lbrakk>inj_on (match A') {<n}; local.stable A' {<n}; length A' = n; set A' \<subseteq> {<n}; aa < n; P\<^sub>a ! aa \<turnstile> match A' aa < match (A[a := A ! a + 1]) aa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix A' a''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A' aa. \<lbrakk>inj_on (match A') {<n}; local.stable A' {<n}; length A' = n; set A' \<subseteq> {<n}; aa < n; P\<^sub>a ! aa \<turnstile> match A' aa < match (A[a := A ! a + 1]) aa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "a'' < n" and A': "length A' = n" "set A' \<subseteq> {<n}" "stable A' {<n}" "inj_on (match A') {<n}"
  and pref_a'': "P\<^sub>a ! a'' \<turnstile> match A' a'' < match ?A a''"
[PROOF STATE]
proof (state)
this:
a'' < n
length A' = n
set A' \<subseteq> {<n}
local.stable A' {<n}
inj_on (match A') {<n}
P\<^sub>a ! a'' \<turnstile> match A' a'' < match (A[a := A ! a + 1]) a''

goal (1 subgoal):
 1. \<And>A' aa. \<lbrakk>inj_on (match A') {<n}; local.stable A' {<n}; length A' = n; set A' \<subseteq> {<n}; aa < n; P\<^sub>a ! aa \<turnstile> match A' aa < match (A[a := A ! a + 1]) aa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
assume [simp]: "a'' = a"
[PROOF STATE]
proof (state)
this:
a'' = a

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
have "A!a < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ! a < n
[PROOF STEP]
using A a
[PROOF STATE]
proof (prove)
using this:
local.wf A
a < n

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
with A A' a pref_a''
[PROOF STATE]
proof (chain)
picking this:
local.wf A
length A' = n
set A' \<subseteq> {<n}
local.stable A' {<n}
inj_on (match A') {<n}
a < n
P\<^sub>a ! a'' \<turnstile> match A' a'' < match (A[a := A ! a + 1]) a''
A ! a < n
[PROOF STEP]
have "P\<^sub>a ! a \<turnstile> match A' a < match A a \<or> match A' a = match A a"
[PROOF STATE]
proof (prove)
using this:
local.wf A
length A' = n
set A' \<subseteq> {<n}
local.stable A' {<n}
inj_on (match A') {<n}
a < n
P\<^sub>a ! a'' \<turnstile> match A' a'' < match (A[a := A ! a + 1]) a''
A ! a < n

goal (1 subgoal):
 1. P\<^sub>a ! a \<turnstile> match A' a < match A a \<or> match A' a = match A a
[PROOF STEP]
apply(auto simp: prefers_def match_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set A' \<subseteq> {<length A'}; local.stable A' {<length A'}; inj_on (match A') {<length A'}; a < length A'; index (P\<^sub>a ! a) (P\<^sub>a ! a ! (A' ! a)) < index (P\<^sub>a ! a) (P\<^sub>a ! a ! Suc (A ! a)); A ! a < length A'; n = length A'; length A = length A'; set A \<subseteq> {<length A'}; P\<^sub>a ! a ! (A' ! a) \<noteq> P\<^sub>a ! a ! (A ! a)\<rbrakk> \<Longrightarrow> index (P\<^sub>a ! a) (P\<^sub>a ! a ! (A' ! a)) < index (P\<^sub>a ! a) (P\<^sub>a ! a ! (A ! a))
[PROOF STEP]
by (smt (verit) P\<^sub>a_set wf_less_n card_atLeastLessThan card_distinct diff_zero index_nth_id
              not_less_eq not_less_less_Suc_eq)
[PROOF STATE]
proof (state)
this:
P\<^sub>a ! a \<turnstile> match A' a < match A a \<or> match A' a = match A a

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
P\<^sub>a ! a \<turnstile> match A' a < match A a \<or> match A' a = match A a

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P\<^sub>a ! a \<turnstile> match A' a < match A a \<Longrightarrow> False
 2. match A' a = match A a \<Longrightarrow> False
[PROOF STEP]
assume "P\<^sub>a ! a \<turnstile> match A' a < match A a "
[PROOF STATE]
proof (state)
this:
P\<^sub>a ! a \<turnstile> match A' a < match A a

goal (2 subgoals):
 1. P\<^sub>a ! a \<turnstile> match A' a < match A a \<Longrightarrow> False
 2. match A' a = match A a \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
P\<^sub>a ! a \<turnstile> match A' a < match A a

goal (1 subgoal):
 1. False
[PROOF STEP]
using opti\<^sub>a A' \<open>a < n\<close>
[PROOF STATE]
proof (prove)
using this:
P\<^sub>a ! a \<turnstile> match A' a < match A a
\<nexists>A'. (local.wf A' \<and> inj_on (match A') {<n}) \<and> local.stable A' {<n} \<and> (\<exists>a<n. P\<^sub>a ! a \<turnstile> match A' a < match A a)
length A' = n
set A' \<subseteq> {<n}
local.stable A' {<n}
inj_on (match A') {<n}
a < n

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

goal (1 subgoal):
 1. match A' a = match A a \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. match A' a = match A a \<Longrightarrow> False
[PROOF STEP]
assume "match A' a = match A a"
[PROOF STATE]
proof (state)
this:
match A' a = match A a

goal (1 subgoal):
 1. match A' a = match A a \<Longrightarrow> False
[PROOF STEP]
have "a \<noteq> a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> a'
[PROOF STEP]
using pref a'
[PROOF STATE]
proof (prove)
using this:
P\<^sub>b ! match A a' \<turnstile> a' < a
a' < n

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

goal (1 subgoal):
 1. match A' a = match A a \<Longrightarrow> False
[PROOF STEP]
hence "blocks A' a' a"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> a'

goal (1 subgoal):
 1. blocks A' a' a
[PROOF STEP]
using opti\<^sub>a pref A' same_match \<open>match A' a = match A a\<close> a a'
[PROOF STATE]
proof (prove)
using this:
a \<noteq> a'
\<nexists>A'. (local.wf A' \<and> inj_on (match A') {<n}) \<and> local.stable A' {<n} \<and> (\<exists>a<n. P\<^sub>a ! a \<turnstile> match A' a < match A a)
P\<^sub>b ! match A a' \<turnstile> a' < a
length A' = n
set A' \<subseteq> {<n}
local.stable A' {<n}
inj_on (match A') {<n}
match A a' = match A a
match A' a = match A a
a < n
a' < n

goal (1 subgoal):
 1. blocks A' a' a
[PROOF STEP]
unfolding blocks_def
[PROOF STATE]
proof (prove)
using this:
a \<noteq> a'
\<nexists>A'. (local.wf A' \<and> inj_on (match A') {<n}) \<and> local.stable A' {<n} \<and> (\<exists>a<n. P\<^sub>a ! a \<turnstile> match A' a < match A a)
P\<^sub>b ! match A a' \<turnstile> a' < a
length A' = n
set A' \<subseteq> {<n}
local.stable A' {<n}
inj_on (match A') {<n}
match A a' = match A a
match A' a = match A a
a < n
a' < n

goal (1 subgoal):
 1. P\<^sub>a ! a' \<turnstile> match A' a < match A' a' \<and> P\<^sub>b ! match A' a \<turnstile> a' < a
[PROOF STEP]
by (metis P\<^sub>a_set atLeast0LessThan match_less_n inj_onD lessThan_iff linorder_neqE_nat nth_index prefers_def)
[PROOF STATE]
proof (state)
this:
blocks A' a' a

goal (1 subgoal):
 1. match A' a = match A a \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
blocks A' a' a

goal (1 subgoal):
 1. False
[PROOF STEP]
using a a' \<open>a \<noteq> a'\<close> A'(3)
[PROOF STATE]
proof (prove)
using this:
blocks A' a' a
a < n
a' < n
a \<noteq> a'
local.stable A' {<n}

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis stable_def atLeastLessThan_iff zero_le)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. a'' \<noteq> a \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a'' \<noteq> a \<Longrightarrow> False
[PROOF STEP]
assume "a'' \<noteq> a"
[PROOF STATE]
proof (state)
this:
a'' \<noteq> a

goal (1 subgoal):
 1. a'' \<noteq> a \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
a'' \<noteq> a

goal (1 subgoal):
 1. False
[PROOF STEP]
using opti\<^sub>a A' pref_a'' \<open>a'' < n\<close>
[PROOF STATE]
proof (prove)
using this:
a'' \<noteq> a
\<nexists>A'. (local.wf A' \<and> inj_on (match A') {<n}) \<and> local.stable A' {<n} \<and> (\<exists>a<n. P\<^sub>a ! a \<turnstile> match A' a < match A a)
length A' = n
set A' \<subseteq> {<n}
local.stable A' {<n}
inj_on (match A') {<n}
P\<^sub>a ! a'' \<turnstile> match A' a'' < match (A[a := A ! a + 1]) a''
a'' < n

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pref_match_stable:
  "\<lbrakk> matching A {<n}; pref_match A {<n} \<rbrakk> \<Longrightarrow> stable A {<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>matching A {<n}; pref_match A {<n}\<rbrakk> \<Longrightarrow> local.stable A {<n}
[PROOF STEP]
unfolding pref_match_def stable_def blocks_def matching_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.wf A \<and> inj_on (match A) {<n}; \<forall>a<n. \<forall>b<n. P\<^sub>a ! a \<turnstile> b < match A a \<longrightarrow> (\<exists>a'\<in>{<n}. b = match A a' \<and> P\<^sub>b ! b \<turnstile> a' < a)\<rbrakk> \<Longrightarrow> \<not> (\<exists>a\<in>{<n}. \<exists>a'\<in>{<n}. a \<noteq> a' \<and> P\<^sub>a ! a \<turnstile> match A a' < match A a \<and> P\<^sub>b ! match A a' \<turnstile> a < a')
[PROOF STEP]
by (metis atLeast0LessThan match_less_n inj_onD lessThan_iff prefers_asym)


[STATEMENT]
lemma invAM_match:
  "\<lbrakk> invAM A M;  a < n \<and> a \<notin> M;  match A a \<notin> match A ` M \<rbrakk> \<Longrightarrow> invAM A (M \<union> {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invAM A M; a < n \<and> a \<notin> M; match A a \<notin> match A ` M\<rbrakk> \<Longrightarrow> invAM A (M \<union> {a})
[PROOF STEP]
by(simp add: pref_match_def)


[STATEMENT]
lemma invAM_swap:
assumes "invAM A M"
assumes a: "a < n \<and> a \<notin> M" and a': "a' \<in> M \<and> match A a' = match A a" and pref: "P\<^sub>b ! match A a' \<turnstile> a < a'"
shows "invAM (A[a' := A!a'+1]) (M - {a'} \<union> {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
have A: "wf A" and M : "M \<subseteq> {<n}" and inj: "inj_on (match A) M" and pref_match: "pref_match A M"
  and "opti\<^sub>a A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.wf A &&& M \<subseteq> {<n}) &&& inj_on (match A) M &&& pref_match A M &&& opti\<^sub>a A
[PROOF STEP]
by(insert \<open>invAM A M\<close>) (auto)
[PROOF STATE]
proof (state)
this:
local.wf A
M \<subseteq> {<n}
inj_on (match A) M
pref_match A M
opti\<^sub>a A

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
have "M \<noteq> {<n}" "a' < n" "a \<noteq> a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<noteq> {<n} &&& a' < n &&& a \<noteq> a'
[PROOF STEP]
using a' a M
[PROOF STATE]
proof (prove)
using this:
a' \<in> M \<and> match A a' = match A a
a < n \<and> a \<notin> M
M \<subseteq> {<n}

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

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
have pref_match': "pref_match' A M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pref_match' A M
[PROOF STEP]
using pref_match pref_match'_iff[OF A]
[PROOF STATE]
proof (prove)
using this:
pref_match A M
pref_match' A ?M = pref_match A ?M

goal (1 subgoal):
 1. pref_match' A M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pref_match' A M

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
let ?A = "A[a' := A!a'+1]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
let ?M = "M - {a'} \<union> {a}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
have neq_a': "\<forall>x. x \<in> ?M \<longrightarrow> a' \<noteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. x \<in> M - {a'} \<union> {a} \<longrightarrow> a' \<noteq> x
[PROOF STEP]
using \<open>a \<noteq> a'\<close>
[PROOF STATE]
proof (prove)
using this:
a \<noteq> a'

goal (1 subgoal):
 1. \<forall>x. x \<in> M - {a'} \<union> {a} \<longrightarrow> a' \<noteq> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> M - {a'} \<union> {a} \<longrightarrow> a' \<noteq> x

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
have \<open>set ?A \<subseteq> {<n}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (A[a' := A ! a' + 1]) \<subseteq> {<n}
[PROOF STEP]
apply(rule set_update_subsetI[OF A[THEN conjunct2]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ! a' + 1 \<in> {<n}
[PROOF STEP]
using more_choices[OF _ M \<open>M \<noteq> {<n}\<close>] A inj pref_match' a' subsetD[OF M, of a']
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>matching ?A M; preferred ?A ?a \<subseteq> match ?A ` M; ?a < n; match ?A ?a \<in> match ?A ` M\<rbrakk> \<Longrightarrow> ?A ! ?a + 1 < n
local.wf A
inj_on (match A) M
pref_match' A M
a' \<in> M \<and> match A a' = match A a
a' \<in> M \<Longrightarrow> a' \<in> {<n}

goal (1 subgoal):
 1. A ! a' + 1 \<in> {<n}
[PROOF STEP]
by(fastforce simp: pref_match'_def)
[PROOF STATE]
proof (state)
this:
set (A[a' := A ! a' + 1]) \<subseteq> {<n}

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
hence "wf ?A"
[PROOF STATE]
proof (prove)
using this:
set (A[a' := A ! a' + 1]) \<subseteq> {<n}

goal (1 subgoal):
 1. local.wf (A[a' := A ! a' + 1])
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
set (A[a' := A ! a' + 1]) \<subseteq> {<n}
local.wf A

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

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.wf (A[a' := A ! a' + 1])

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
have "inj_on (match ?A) ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (match (A[a' := A ! a' + 1])) (M - {a'} \<union> {a})
[PROOF STEP]
using a a' inj
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> M
a' \<in> M \<and> match A a' = match A a
inj_on (match A) M

goal (1 subgoal):
 1. inj_on (match (A[a' := A ! a' + 1])) (M - {a'} \<union> {a})
[PROOF STEP]
by(simp add: match_def inj_on_def)(metis Diff_iff insert_iff nth_list_update_neq)
[PROOF STATE]
proof (state)
this:
inj_on (match (A[a' := A ! a' + 1])) (M - {a'} \<union> {a})

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inj_on (match (A[a' := A ! a' + 1])) (M - {a'} \<union> {a})

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
have "pref_match' ?A ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pref_match' (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
using a a' pref_match' A pref \<open>a' < n\<close>
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> M
a' \<in> M \<and> match A a' = match A a
pref_match' A M
local.wf A
P\<^sub>b ! match A a' \<turnstile> a < a'
a' < n

goal (1 subgoal):
 1. pref_match' (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
apply(simp add: pref_match'_def match_upd_neq neq_a' Ball_def Bex_def image_iff imp_ex nth_list_update less_Suc_eq
            flip: match_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < n \<and> a \<notin> M; a' \<in> M \<and> match A a' = match A a; \<forall>a<n. \<forall>x<A ! a. \<exists>xa. xa \<in> M \<and> P\<^sub>a ! a ! x = match A xa \<and> P\<^sub>b ! (P\<^sub>a ! a ! x) \<turnstile> xa < a; local.wf A; P\<^sub>b ! match A a \<turnstile> a < a'; a' < n\<rbrakk> \<Longrightarrow> \<forall>aa. (a' = aa \<longrightarrow> (\<forall>x. (x < A ! aa \<longrightarrow> (\<exists>xa. (xa = a \<or> xa \<in> M \<and> xa \<noteq> aa) \<and> P\<^sub>a ! aa ! x = match A xa \<and> P\<^sub>b ! (P\<^sub>a ! aa ! x) \<turnstile> xa < aa)) \<and> (x = A ! aa \<longrightarrow> (\<exists>x. (x = a \<or> x \<in> M \<and> x \<noteq> aa) \<and> match A aa = match A x \<and> P\<^sub>b ! match A aa \<turnstile> x < aa)))) \<and> (a' \<noteq> aa \<longrightarrow> aa < n \<longrightarrow> (\<forall>x<A ! aa. \<exists>xa. (xa = a \<or> xa \<in> M \<and> xa \<noteq> a') \<and> P\<^sub>a ! aa ! x = match A xa \<and> P\<^sub>b ! (P\<^sub>a ! aa ! x) \<turnstile> xa < aa))
[PROOF STEP]
by (metis prefers_trans)
[PROOF STATE]
proof (state)
this:
pref_match' (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})

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

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
have "opti\<^sub>a ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. opti\<^sub>a (A[a' := A ! a' + 1])
[PROOF STEP]
using opti\<^sub>a_inv[OF A \<open>a' < n\<close> _ _ _ \<open>opti\<^sub>a A\<close>] a a'[THEN conjunct2] pref
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a' < n; match A ?a' = match A a'; P\<^sub>b ! match A ?a' \<turnstile> ?a' < a'\<rbrakk> \<Longrightarrow> opti\<^sub>a (A[a' := A ! a' + 1])
a < n \<and> a \<notin> M
match A a' = match A a
P\<^sub>b ! match A a' \<turnstile> a < a'

goal (1 subgoal):
 1. opti\<^sub>a (A[a' := A ! a' + 1])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
opti\<^sub>a (A[a' := A ! a' + 1])

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
local.wf (A[a' := A ! a' + 1])
inj_on (match (A[a' := A ! a' + 1])) (M - {a'} \<union> {a})
pref_match' (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
opti\<^sub>a (A[a' := A ! a' + 1])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.wf (A[a' := A ! a' + 1])
inj_on (match (A[a' := A ! a' + 1])) (M - {a'} \<union> {a})
pref_match' (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
opti\<^sub>a (A[a' := A ! a' + 1])

goal (1 subgoal):
 1. invAM (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
[PROOF STEP]
using a a' M pref_match'_iff
[PROOF STATE]
proof (prove)
using this:
local.wf (A[a' := A ! a' + 1])
inj_on (match (A[a' := A ! a' + 1])) (M - {a'} \<union> {a})
pref_match' (A[a' := A ! a' + 1]) (M - {a'} \<union> {a})
opti\<^sub>a (A[a' := A ! a' + 1])
a < n \<and> a \<notin> M
a' \<in> M \<and> match A a' = match A a
M \<subseteq> {<n}
local.wf ?A \<Longrightarrow> pref_match' ?A ?M = pref_match ?A ?M

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invAM_next:
assumes "invAM A M"
assumes a: "a < n \<and> a \<notin> M" and a': "a' \<in> M \<and> match A a' = match A a" and pref: "\<not> P\<^sub>b ! match A a' \<turnstile> a < a'"
shows "invAM (A[a := A!a + 1]) M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
have A: "wf A" and M : "M \<subseteq> {<n}" and inj: "inj_on (match A) M" and pref_match: "pref_match A M"
  and opti\<^sub>a: "opti\<^sub>a A" and "a' < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.wf A &&& M \<subseteq> {<n} &&& inj_on (match A) M) &&& pref_match A M &&& opti\<^sub>a A &&& a' < n
[PROOF STEP]
by(insert \<open>invAM A M\<close> a') (auto)
[PROOF STATE]
proof (state)
this:
local.wf A
M \<subseteq> {<n}
inj_on (match A) M
pref_match A M
opti\<^sub>a A
a' < n

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
hence pref': "P\<^sub>b ! match A a' \<turnstile> a' < a"
[PROOF STATE]
proof (prove)
using this:
local.wf A
M \<subseteq> {<n}
inj_on (match A) M
pref_match A M
opti\<^sub>a A
a' < n

goal (1 subgoal):
 1. P\<^sub>b ! match A a' \<turnstile> a' < a
[PROOF STEP]
using pref a a' P\<^sub>b_set
[PROOF STATE]
proof (prove)
using this:
local.wf A
M \<subseteq> {<n}
inj_on (match A) M
pref_match A M
opti\<^sub>a A
a' < n
\<not> P\<^sub>b ! match A a' \<turnstile> a < a'
a < n \<and> a \<notin> M
a' \<in> M \<and> match A a' = match A a
?b < n \<Longrightarrow> length (P\<^sub>b ! ?b) = n \<and> set (P\<^sub>b ! ?b) = {<n}

goal (1 subgoal):
 1. P\<^sub>b ! match A a' \<turnstile> a' < a
[PROOF STEP]
unfolding prefers_def
[PROOF STATE]
proof (prove)
using this:
local.wf A
M \<subseteq> {<n}
inj_on (match A) M
pref_match A M
opti\<^sub>a A
a' < n
\<not> index (P\<^sub>b ! match A a') a < index (P\<^sub>b ! match A a') a'
a < n \<and> a \<notin> M
a' \<in> M \<and> match A a' = match A a
?b < n \<Longrightarrow> length (P\<^sub>b ! ?b) = n \<and> set (P\<^sub>b ! ?b) = {<n}

goal (1 subgoal):
 1. index (P\<^sub>b ! match A a') a' < index (P\<^sub>b ! match A a') a
[PROOF STEP]
by (metis match_def match_less_n index_eq_index_conv linorder_less_linear subsetD)
[PROOF STATE]
proof (state)
this:
P\<^sub>b ! match A a' \<turnstile> a' < a

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
have "M \<noteq> {<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<noteq> {<n}
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> M

goal (1 subgoal):
 1. M \<noteq> {<n}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
M \<noteq> {<n}

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
have neq_a: "\<forall>x. x\<in> M \<longrightarrow> a \<noteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. x \<in> M \<longrightarrow> a \<noteq> x
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> M

goal (1 subgoal):
 1. \<forall>x. x \<in> M \<longrightarrow> a \<noteq> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> M \<longrightarrow> a \<noteq> x

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
have pref_match': "pref_match' A M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pref_match' A M
[PROOF STEP]
using pref_match pref_match'_iff[OF A,of M]
[PROOF STATE]
proof (prove)
using this:
pref_match A M
pref_match' A M = pref_match A M

goal (1 subgoal):
 1. pref_match' A M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pref_match' A M

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
hence "\<forall>a<n. preferred A a \<subseteq> match A ` M"
[PROOF STATE]
proof (prove)
using this:
pref_match' A M

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

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

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
hence "A!a + 1 < n"
[PROOF STATE]
proof (prove)
using this:
\<forall>a<n. preferred A a \<subseteq> match A ` M

goal (1 subgoal):
 1. A ! a + 1 < n
[PROOF STEP]
using more_choices[OF _ M \<open>M \<noteq> {<n}\<close>] A inj a a'
[PROOF STATE]
proof (prove)
using this:
\<forall>a<n. preferred A a \<subseteq> match A ` M
\<lbrakk>matching ?A M; preferred ?A ?a \<subseteq> match ?A ` M; ?a < n; match ?A ?a \<in> match ?A ` M\<rbrakk> \<Longrightarrow> ?A ! ?a + 1 < n
local.wf A
inj_on (match A) M
a < n \<and> a \<notin> M
a' \<in> M \<and> match A a' = match A a

goal (1 subgoal):
 1. A ! a + 1 < n
[PROOF STEP]
unfolding matching_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a<n. preferred A a \<subseteq> match A ` M
\<lbrakk>local.wf ?A \<and> inj_on (match ?A) M; preferred ?A ?a \<subseteq> match ?A ` M; ?a < n; match ?A ?a \<in> match ?A ` M\<rbrakk> \<Longrightarrow> ?A ! ?a + 1 < n
local.wf A
inj_on (match A) M
a < n \<and> a \<notin> M
a' \<in> M \<and> match A a' = match A a

goal (1 subgoal):
 1. A ! a + 1 < n
[PROOF STEP]
by (metis (no_types, lifting) imageI)
[PROOF STATE]
proof (state)
this:
A ! a + 1 < n

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
let ?A = "A[a := A!a+1]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
have "wf ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.wf (A[a := A ! a + 1])
[PROOF STEP]
using A \<open>A!a + 1 < n\<close>
[PROOF STATE]
proof (prove)
using this:
local.wf A
A ! a + 1 < n

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

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

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
have "inj_on (match ?A) M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (match (A[a := A ! a + 1])) M
[PROOF STEP]
using a inj
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> M
inj_on (match A) M

goal (1 subgoal):
 1. inj_on (match (A[a := A ! a + 1])) M
[PROOF STEP]
by(simp add: match_def inj_on_def) (metis nth_list_update_neq)
[PROOF STATE]
proof (state)
this:
inj_on (match (A[a := A ! a + 1])) M

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

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
have "pref_match' ?A M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pref_match' (A[a := A ! a + 1]) M
[PROOF STEP]
using a pref_match' pref' A a' neq_a
[PROOF STATE]
proof (prove)
using this:
a < n \<and> a \<notin> M
pref_match' A M
P\<^sub>b ! match A a' \<turnstile> a' < a
local.wf A
a' \<in> M \<and> match A a' = match A a
\<forall>x. x \<in> M \<longrightarrow> a \<noteq> x

goal (1 subgoal):
 1. pref_match' (A[a := A ! a + 1]) M
[PROOF STEP]
by(auto simp: match_upd_neq pref_match'_def Ball_def Bex_def image_iff nth_list_update imp_ex less_Suc_eq
            simp flip: match_def)
[PROOF STATE]
proof (state)
this:
pref_match' (A[a := A ! a + 1]) M

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

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
have  "opti\<^sub>a ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. opti\<^sub>a (A[a := A ! a + 1])
[PROOF STEP]
using opti\<^sub>a_inv[OF A conjunct1[OF a] \<open>a' < n\<close> conjunct2[OF a'] pref' opti\<^sub>a]
[PROOF STATE]
proof (prove)
using this:
opti\<^sub>a (A[a := A ! a + 1])

goal (1 subgoal):
 1. opti\<^sub>a (A[a := A ! a + 1])
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
opti\<^sub>a (A[a := A ! a + 1])

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
local.wf (A[a := A ! a + 1])
inj_on (match (A[a := A ! a + 1])) M
pref_match' (A[a := A ! a + 1]) M
opti\<^sub>a (A[a := A ! a + 1])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.wf (A[a := A ! a + 1])
inj_on (match (A[a := A ! a + 1])) M
pref_match' (A[a := A ! a + 1]) M
opti\<^sub>a (A[a := A ! a + 1])

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
using M
[PROOF STATE]
proof (prove)
using this:
local.wf (A[a := A ! a + 1])
inj_on (match (A[a := A ! a + 1])) M
pref_match' (A[a := A ! a + 1]) M
opti\<^sub>a (A[a := A ! a + 1])
M \<subseteq> {<n}

goal (1 subgoal):
 1. invAM (A[a := A ! a + 1]) M
[PROOF STEP]
by (simp add: pref_match'_iff)
[PROOF STATE]
proof (state)
this:
invAM (A[a := A ! a + 1]) M

goal:
No subgoals!
[PROOF STEP]
qed