[STATEMENT]
lemma nth_least_ext_strict_mono:
    assumes "k < l"
    shows "nth_least_ext s k < nth_least_ext s l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
proof (cases "enat l < esize s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. enat l < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat l < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
enat l < esize s

goal (2 subgoals):
 1. enat l < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat l < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have 1: "enat k < esize s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat k < esize s
[PROOF STEP]
using assms True
[PROOF STATE]
proof (prove)
using this:
k < l
enat l < esize s

goal (1 subgoal):
 1. enat k < esize s
[PROOF STEP]
by (metis enat_ord_simps(2) less_trans)
[PROOF STATE]
proof (state)
this:
enat k < esize s

goal (2 subgoals):
 1. enat l < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat l < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
using nth_least_strict_mono assms True 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>enat ?l < esize ?A; ?k < ?l\<rbrakk> \<Longrightarrow> nth_least ?A ?k < nth_least ?A ?l
k < l
enat l < esize s
enat k < esize s

goal (1 subgoal):
 1. nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nth_least_ext s k < nth_least_ext s l

goal (1 subgoal):
 1. \<not> enat l < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> enat l < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> enat l < esize s

goal (1 subgoal):
 1. \<not> enat l < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have 1: "finite s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite s
[PROOF STEP]
using False esize_infinite_enat
[PROOF STATE]
proof (prove)
using this:
\<not> enat l < esize s
infinite ?A \<Longrightarrow> enat ?k < esize ?A

goal (1 subgoal):
 1. finite s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite s

goal (1 subgoal):
 1. \<not> enat l < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have 2: "enat l \<ge> esize s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. esize s \<le> enat l
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> enat l < esize s

goal (1 subgoal):
 1. esize s \<le> enat l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
esize s \<le> enat l

goal (1 subgoal):
 1. \<not> enat l < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have 3: "l \<ge> card s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card s \<le> l
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
finite s
esize s \<le> enat l

goal (1 subgoal):
 1. card s \<le> l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card s \<le> l

goal (1 subgoal):
 1. \<not> enat l < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
proof (cases "enat k < esize s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
enat k < esize s

goal (2 subgoals):
 1. enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have 4: "s \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> {}
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
enat k < esize s

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

goal (2 subgoals):
 1. enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have "nth_least_ext s k = nth_least s k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least_ext s k = nth_least s k
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
enat k < esize s

goal (1 subgoal):
 1. nth_least_ext s k = nth_least s k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nth_least_ext s k = nth_least s k

goal (2 subgoals):
 1. enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nth_least_ext s k = nth_least s k

goal (2 subgoals):
 1. enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have "\<dots> \<le> Max s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least s k \<le> Max s
[PROOF STEP]
using nth_least_le_Max 1 4 True
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?A \<noteq> {}; enat ?n < esize ?A\<rbrakk> \<Longrightarrow> nth_least ?A ?n \<le> Max ?A
finite s
s \<noteq> {}
enat k < esize s

goal (1 subgoal):
 1. nth_least s k \<le> Max s
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
nth_least s k \<le> Max s

goal (2 subgoals):
 1. enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nth_least s k \<le> Max s

goal (2 subgoals):
 1. enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have "\<dots> < Suc (Max s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max s < Suc (Max s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max s < Suc (Max s)

goal (2 subgoals):
 1. enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Max s < Suc (Max s)

goal (2 subgoals):
 1. enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have "\<dots> \<le> Suc (Max s + (l - card s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (Max s) \<le> Suc (Max s + (l - card s))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (Max s) \<le> Suc (Max s + (l - card s))

goal (2 subgoals):
 1. enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc (Max s) \<le> Suc (Max s + (l - card s))

goal (2 subgoals):
 1. enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have "Suc (Max s + (l - card s)) = nth_least_ext s l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (Max s + (l - card s)) = nth_least_ext s l
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
esize s \<le> enat l

goal (1 subgoal):
 1. Suc (Max s + (l - card s)) = nth_least_ext s l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (Max s + (l - card s)) = nth_least_ext s l

goal (2 subgoals):
 1. enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
 2. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nth_least_ext s k < nth_least_ext s l

goal (1 subgoal):
 1. nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
nth_least_ext s k < nth_least_ext s l

goal (1 subgoal):
 1. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> enat k < esize s

goal (1 subgoal):
 1. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have 4: "enat k \<ge> esize s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. esize s \<le> enat k
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> enat k < esize s

goal (1 subgoal):
 1. esize s \<le> enat k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
esize s \<le> enat k

goal (1 subgoal):
 1. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have 5: "k \<ge> card s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card s \<le> k
[PROOF STEP]
using 1 4
[PROOF STATE]
proof (prove)
using this:
finite s
esize s \<le> enat k

goal (1 subgoal):
 1. card s \<le> k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card s \<le> k

goal (1 subgoal):
 1. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have "nth_least_ext s k = Suc (Max s + (k - card s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least_ext s k = Suc (Max s + (k - card s))
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
esize s \<le> enat k

goal (1 subgoal):
 1. nth_least_ext s k = Suc (Max s + (k - card s))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nth_least_ext s k = Suc (Max s + (k - card s))

goal (1 subgoal):
 1. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nth_least_ext s k = Suc (Max s + (k - card s))

goal (1 subgoal):
 1. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have "\<dots> < Suc (Max s + (l - card s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (Max s + (k - card s)) < Suc (Max s + (l - card s))
[PROOF STEP]
using assms 5
[PROOF STATE]
proof (prove)
using this:
k < l
card s \<le> k

goal (1 subgoal):
 1. Suc (Max s + (k - card s)) < Suc (Max s + (l - card s))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (Max s + (k - card s)) < Suc (Max s + (l - card s))

goal (1 subgoal):
 1. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc (Max s + (k - card s)) < Suc (Max s + (l - card s))

goal (1 subgoal):
 1. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
have "\<dots> = nth_least_ext s l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (Max s + (l - card s)) = nth_least_ext s l
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
esize s \<le> enat l

goal (1 subgoal):
 1. Suc (Max s + (l - card s)) = nth_least_ext s l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (Max s + (l - card s)) = nth_least_ext s l

goal (1 subgoal):
 1. \<not> enat k < esize s \<Longrightarrow> nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nth_least_ext s k < nth_least_ext s l

goal (1 subgoal):
 1. nth_least_ext s k < nth_least_ext s l
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
nth_least_ext s k < nth_least_ext s l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nth_least_ext s k < nth_least_ext s l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stutter_selectionI[intro]:
    assumes "0 \<in> s"
    assumes "\<And> k i. enat i < llength w \<Longrightarrow> enat (Suc k) < esize s \<Longrightarrow>
      nth_least s k < i \<Longrightarrow> i < nth_least s (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least s k"
    assumes "\<And> i. enat i < llength w \<Longrightarrow> finite s \<Longrightarrow> Max s < i \<Longrightarrow> w ?! i = w ?! Max s"
    shows "stutter_selection s w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_selection s w
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<in> s
\<lbrakk>enat ?i < llength w; enat (Suc ?k) < esize s; nth_least s ?k < ?i; ?i < nth_least s (Suc ?k)\<rbrakk> \<Longrightarrow> w ?! ?i = w ?! nth_least s ?k
\<lbrakk>enat ?i < llength w; finite s; Max s < ?i\<rbrakk> \<Longrightarrow> w ?! ?i = w ?! Max s

goal (1 subgoal):
 1. stutter_selection s w
[PROOF STEP]
unfolding stutter_selection_def
[PROOF STATE]
proof (prove)
using this:
0 \<in> s
\<lbrakk>enat ?i < llength w; enat (Suc ?k) < esize s; nth_least s ?k < ?i; ?i < nth_least s (Suc ?k)\<rbrakk> \<Longrightarrow> w ?! ?i = w ?! nth_least s ?k
\<lbrakk>enat ?i < llength w; finite s; Max s < ?i\<rbrakk> \<Longrightarrow> w ?! ?i = w ?! Max s

goal (1 subgoal):
 1. 0 \<in> s \<and> (\<forall>k i. enat i < llength w \<longrightarrow> enat (Suc k) < esize s \<longrightarrow> nth_least s k < i \<longrightarrow> i < nth_least s (Suc k) \<longrightarrow> w ?! i = w ?! nth_least s k) \<and> (\<forall>i. enat i < llength w \<longrightarrow> finite s \<longrightarrow> Max s < i \<longrightarrow> w ?! i = w ?! Max s)
[PROOF STEP]
by auto


[STATEMENT]
lemma stutter_selectionD_0[dest]:
    assumes "stutter_selection s w"
    shows "0 \<in> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<in> s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
stutter_selection s w

goal (1 subgoal):
 1. 0 \<in> s
[PROOF STEP]
unfolding stutter_selection_def
[PROOF STATE]
proof (prove)
using this:
0 \<in> s \<and> (\<forall>k i. enat i < llength w \<longrightarrow> enat (Suc k) < esize s \<longrightarrow> nth_least s k < i \<longrightarrow> i < nth_least s (Suc k) \<longrightarrow> w ?! i = w ?! nth_least s k) \<and> (\<forall>i. enat i < llength w \<longrightarrow> finite s \<longrightarrow> Max s < i \<longrightarrow> w ?! i = w ?! Max s)

goal (1 subgoal):
 1. 0 \<in> s
[PROOF STEP]
by auto


[STATEMENT]
lemma stutter_selectionD_inside[dest]:
    assumes "stutter_selection s w"
    assumes "enat i < llength w" "enat (Suc k) < esize s"
    assumes "nth_least s k < i" "i < nth_least s (Suc k)"
    shows "w ?! i = w ?! nth_least s k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w ?! i = w ?! nth_least s k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
stutter_selection s w
enat i < llength w
enat (Suc k) < esize s
nth_least s k < i
i < nth_least s (Suc k)

goal (1 subgoal):
 1. w ?! i = w ?! nth_least s k
[PROOF STEP]
unfolding stutter_selection_def
[PROOF STATE]
proof (prove)
using this:
0 \<in> s \<and> (\<forall>k i. enat i < llength w \<longrightarrow> enat (Suc k) < esize s \<longrightarrow> nth_least s k < i \<longrightarrow> i < nth_least s (Suc k) \<longrightarrow> w ?! i = w ?! nth_least s k) \<and> (\<forall>i. enat i < llength w \<longrightarrow> finite s \<longrightarrow> Max s < i \<longrightarrow> w ?! i = w ?! Max s)
enat i < llength w
enat (Suc k) < esize s
nth_least s k < i
i < nth_least s (Suc k)

goal (1 subgoal):
 1. w ?! i = w ?! nth_least s k
[PROOF STEP]
by auto


[STATEMENT]
lemma stutter_selectionD_infinite[dest]:
    assumes "stutter_selection s w"
    assumes "enat i < llength w" "finite s" "Max s < i"
    shows "w ?! i = w ?! Max s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w ?! i = w ?! Max s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
stutter_selection s w
enat i < llength w
finite s
Max s < i

goal (1 subgoal):
 1. w ?! i = w ?! Max s
[PROOF STEP]
unfolding stutter_selection_def
[PROOF STATE]
proof (prove)
using this:
0 \<in> s \<and> (\<forall>k i. enat i < llength w \<longrightarrow> enat (Suc k) < esize s \<longrightarrow> nth_least s k < i \<longrightarrow> i < nth_least s (Suc k) \<longrightarrow> w ?! i = w ?! nth_least s k) \<and> (\<forall>i. enat i < llength w \<longrightarrow> finite s \<longrightarrow> Max s < i \<longrightarrow> w ?! i = w ?! Max s)
enat i < llength w
finite s
Max s < i

goal (1 subgoal):
 1. w ?! i = w ?! Max s
[PROOF STEP]
by auto


[STATEMENT]
lemma stutter_selection_stutter_sampler[intro]:
    assumes "linfinite w" "stutter_selection s w"
    shows "stutter_sampler (nth_least_ext s) (lnth w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_sampler (nth_least_ext s) ((?!) w)
[PROOF STEP]
unfolding stutter_sampler_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least_ext s 0 = 0 \<and> strict_mono (nth_least_ext s) \<and> (\<forall>k n. nth_least_ext s k < n \<and> n < nth_least_ext s (Suc k) \<longrightarrow> w ?! n = w ?! nth_least_ext s k)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. nth_least_ext s 0 = 0
 2. strict_mono (nth_least_ext s)
 3. \<And>k n. \<lbrakk>nth_least_ext s k < n; n < nth_least_ext s (Suc k)\<rbrakk> \<Longrightarrow> w ?! n = w ?! nth_least_ext s k
[PROOF STEP]
show "nth_least_ext s 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least_ext s 0 = 0
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
stutter_selection s w

goal (1 subgoal):
 1. nth_least_ext s 0 = 0
[PROOF STEP]
by (cases "enat 0 < esize s", auto)
[PROOF STATE]
proof (state)
this:
nth_least_ext s 0 = 0

goal (2 subgoals):
 1. strict_mono (nth_least_ext s)
 2. \<And>k n. \<lbrakk>nth_least_ext s k < n; n < nth_least_ext s (Suc k)\<rbrakk> \<Longrightarrow> w ?! n = w ?! nth_least_ext s k
[PROOF STEP]
show "strict_mono (nth_least_ext s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_mono (nth_least_ext s)
[PROOF STEP]
using strict_monoI nth_least_ext_strict_mono
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x < y \<Longrightarrow> ?f x < ?f y) \<Longrightarrow> strict_mono ?f
?k < ?l \<Longrightarrow> nth_least_ext ?s ?k < nth_least_ext ?s ?l

goal (1 subgoal):
 1. strict_mono (nth_least_ext s)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
strict_mono (nth_least_ext s)

goal (1 subgoal):
 1. \<And>k n. \<lbrakk>nth_least_ext s k < n; n < nth_least_ext s (Suc k)\<rbrakk> \<Longrightarrow> w ?! n = w ?! nth_least_ext s k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k n. \<lbrakk>nth_least_ext s k < n; n < nth_least_ext s (Suc k)\<rbrakk> \<Longrightarrow> w ?! n = w ?! nth_least_ext s k
[PROOF STEP]
fix k i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k n. \<lbrakk>nth_least_ext s k < n; n < nth_least_ext s (Suc k)\<rbrakk> \<Longrightarrow> w ?! n = w ?! nth_least_ext s k
[PROOF STEP]
assume 1: "nth_least_ext s k < i" "i < nth_least_ext s (Suc k)"
[PROOF STATE]
proof (state)
this:
nth_least_ext s k < i
i < nth_least_ext s (Suc k)

goal (1 subgoal):
 1. \<And>k n. \<lbrakk>nth_least_ext s k < n; n < nth_least_ext s (Suc k)\<rbrakk> \<Longrightarrow> w ?! n = w ?! nth_least_ext s k
[PROOF STEP]
show "w ?! i = w ?! nth_least_ext s k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
proof (cases "enat (Suc k)" "esize s" rule: linorder_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. enat (Suc k) < esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 3. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
enat (Suc k) < esize s

goal (3 subgoals):
 1. enat (Suc k) < esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 3. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have "w ?! i = w ?! nth_least s k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w ?! i = w ?! nth_least s k
[PROOF STEP]
proof (rule stutter_selectionD_inside)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. stutter_selection s w
 2. enat i < llength w
 3. enat (Suc k) < esize s
 4. nth_least s k < i
 5. i < nth_least s (Suc k)
[PROOF STEP]
show "stutter_selection s w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_selection s w
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
stutter_selection s w

goal (1 subgoal):
 1. stutter_selection s w
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
stutter_selection s w

goal (4 subgoals):
 1. enat i < llength w
 2. enat (Suc k) < esize s
 3. nth_least s k < i
 4. i < nth_least s (Suc k)
[PROOF STEP]
show "enat i < llength w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat i < llength w
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
linfinite w

goal (1 subgoal):
 1. enat i < llength w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enat i < llength w

goal (3 subgoals):
 1. enat (Suc k) < esize s
 2. nth_least s k < i
 3. i < nth_least s (Suc k)
[PROOF STEP]
show "enat (Suc k) < esize s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat (Suc k) < esize s
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
enat (Suc k) < esize s

goal (1 subgoal):
 1. enat (Suc k) < esize s
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
enat (Suc k) < esize s

goal (2 subgoals):
 1. nth_least s k < i
 2. i < nth_least s (Suc k)
[PROOF STEP]
show "nth_least s k < i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least s k < i
[PROOF STEP]
using 1(1) less
[PROOF STATE]
proof (prove)
using this:
nth_least_ext s k < i
enat (Suc k) < esize s

goal (1 subgoal):
 1. nth_least s k < i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nth_least s k < i

goal (1 subgoal):
 1. i < nth_least s (Suc k)
[PROOF STEP]
show "i < nth_least s (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < nth_least s (Suc k)
[PROOF STEP]
using 1(2) less
[PROOF STATE]
proof (prove)
using this:
i < nth_least_ext s (Suc k)
enat (Suc k) < esize s

goal (1 subgoal):
 1. i < nth_least s (Suc k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < nth_least s (Suc k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
w ?! i = w ?! nth_least s k

goal (3 subgoals):
 1. enat (Suc k) < esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 3. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w ?! i = w ?! nth_least s k

goal (3 subgoals):
 1. enat (Suc k) < esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 3. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have "w ?! nth_least s k = w ?! nth_least_ext s k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w ?! nth_least s k = w ?! nth_least_ext s k
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
enat (Suc k) < esize s

goal (1 subgoal):
 1. w ?! nth_least s k = w ?! nth_least_ext s k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w ?! nth_least s k = w ?! nth_least_ext s k

goal (3 subgoals):
 1. enat (Suc k) < esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 3. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w ?! i = w ?! nth_least_ext s k

goal (1 subgoal):
 1. w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
w ?! i = w ?! nth_least_ext s k

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
case equal
[PROOF STATE]
proof (state)
this:
enat (Suc k) = esize s

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have 2: "enat k < esize s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat k < esize s
[PROOF STEP]
using equal
[PROOF STATE]
proof (prove)
using this:
enat (Suc k) = esize s

goal (1 subgoal):
 1. enat k < esize s
[PROOF STEP]
by (metis enat_ord_simps(2) lessI)
[PROOF STATE]
proof (state)
this:
enat k < esize s

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have 3: "finite s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite s
[PROOF STEP]
using equal
[PROOF STATE]
proof (prove)
using this:
enat (Suc k) = esize s

goal (1 subgoal):
 1. finite s
[PROOF STEP]
by (metis esize_infinite_enat less_irrefl)
[PROOF STATE]
proof (state)
this:
finite s

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have 4: "\<And> i. i > Max s \<Longrightarrow> w ?! i = w ?! Max s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. Max s < i \<Longrightarrow> w ?! i = w ?! Max s
[PROOF STEP]
using assms 3
[PROOF STATE]
proof (prove)
using this:
linfinite w
stutter_selection s w
finite s

goal (1 subgoal):
 1. \<And>i. Max s < i \<Longrightarrow> w ?! i = w ?! Max s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max s < ?i \<Longrightarrow> w ?! ?i = w ?! Max s

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have 5: "k = card s - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = card s - 1
[PROOF STEP]
using equal 3
[PROOF STATE]
proof (prove)
using this:
enat (Suc k) = esize s
finite s

goal (1 subgoal):
 1. k = card s - 1
[PROOF STEP]
by (metis diff_Suc_1 enat.inject esize_set.simps(1))
[PROOF STATE]
proof (state)
this:
k = card s - 1

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have "Max s = nth_least s (card s - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max s = nth_least s (card s - 1)
[PROOF STEP]
using nth_least_Max 3 assms(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> nth_least ?A (card ?A - 1) = Max ?A
finite s
stutter_selection s w

goal (1 subgoal):
 1. Max s = nth_least s (card s - 1)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Max s = nth_least s (card s - 1)

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Max s = nth_least s (card s - 1)

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have "\<dots> = nth_least s k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least s (card s - 1) = nth_least s k
[PROOF STEP]
unfolding 5
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least s (card s - 1) = nth_least s (card s - 1)
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
nth_least s (card s - 1) = nth_least s k

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nth_least s (card s - 1) = nth_least s k

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have "\<dots> = nth_least_ext s k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least s k = nth_least_ext s k
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
enat k < esize s

goal (1 subgoal):
 1. nth_least s k = nth_least_ext s k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nth_least s k = nth_least_ext s k

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Max s = nth_least_ext s k
[PROOF STEP]
have 6: "Max s = nth_least_ext s k"
[PROOF STATE]
proof (prove)
using this:
Max s = nth_least_ext s k

goal (1 subgoal):
 1. Max s = nth_least_ext s k
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
Max s = nth_least_ext s k

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have "w ?! i = w ?! Max s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w ?! i = w ?! Max s
[PROOF STEP]
using 1(1) 4 6
[PROOF STATE]
proof (prove)
using this:
nth_least_ext s k < i
Max s < ?i \<Longrightarrow> w ?! ?i = w ?! Max s
Max s = nth_least_ext s k

goal (1 subgoal):
 1. w ?! i = w ?! Max s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w ?! i = w ?! Max s

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w ?! i = w ?! Max s

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have "\<dots> = w ?! nth_least_ext s k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w ?! Max s = w ?! nth_least_ext s k
[PROOF STEP]
unfolding 6
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w ?! nth_least_ext s k = w ?! nth_least_ext s k
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
w ?! Max s = w ?! nth_least_ext s k

goal (2 subgoals):
 1. enat (Suc k) = esize s \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
 2. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w ?! i = w ?! nth_least_ext s k

goal (1 subgoal):
 1. w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
w ?! i = w ?! nth_least_ext s k

goal (1 subgoal):
 1. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
case greater
[PROOF STATE]
proof (state)
this:
esize s < enat (Suc k)

goal (1 subgoal):
 1. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have 2: "enat k \<ge> esize s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. esize s \<le> enat k
[PROOF STEP]
using greater
[PROOF STATE]
proof (prove)
using this:
esize s < enat (Suc k)

goal (1 subgoal):
 1. esize s \<le> enat k
[PROOF STEP]
by (metis Suc_ile_eq not_le)
[PROOF STATE]
proof (state)
this:
esize s \<le> enat k

goal (1 subgoal):
 1. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have 3: "finite s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite s
[PROOF STEP]
using greater
[PROOF STATE]
proof (prove)
using this:
esize s < enat (Suc k)

goal (1 subgoal):
 1. finite s
[PROOF STEP]
by (metis esize_infinite_enat less_asym)
[PROOF STATE]
proof (state)
this:
finite s

goal (1 subgoal):
 1. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have 4: "\<And> i. i > Max s \<Longrightarrow> w ?! i = w ?! Max s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. Max s < i \<Longrightarrow> w ?! i = w ?! Max s
[PROOF STEP]
using assms 3
[PROOF STATE]
proof (prove)
using this:
linfinite w
stutter_selection s w
finite s

goal (1 subgoal):
 1. \<And>i. Max s < i \<Longrightarrow> w ?! i = w ?! Max s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max s < ?i \<Longrightarrow> w ?! ?i = w ?! Max s

goal (1 subgoal):
 1. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have "w ?! i = w ?! Max s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w ?! i = w ?! Max s
[PROOF STEP]
using 1(1) 2 4
[PROOF STATE]
proof (prove)
using this:
nth_least_ext s k < i
esize s \<le> enat k
Max s < ?i \<Longrightarrow> w ?! ?i = w ?! Max s

goal (1 subgoal):
 1. w ?! i = w ?! Max s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w ?! i = w ?! Max s

goal (1 subgoal):
 1. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w ?! i = w ?! Max s

goal (1 subgoal):
 1. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have "\<dots> = w ?! Suc (Max s + (k - card s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w ?! Max s = w ?! Suc (Max s + (k - card s))
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
Max s < ?i \<Longrightarrow> w ?! ?i = w ?! Max s

goal (1 subgoal):
 1. w ?! Max s = w ?! Suc (Max s + (k - card s))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w ?! Max s = w ?! Suc (Max s + (k - card s))

goal (1 subgoal):
 1. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w ?! Max s = w ?! Suc (Max s + (k - card s))

goal (1 subgoal):
 1. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
have "\<dots> = w ?! nth_least_ext s k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w ?! Suc (Max s + (k - card s)) = w ?! nth_least_ext s k
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
esize s \<le> enat k

goal (1 subgoal):
 1. w ?! Suc (Max s + (k - card s)) = w ?! nth_least_ext s k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w ?! Suc (Max s + (k - card s)) = w ?! nth_least_ext s k

goal (1 subgoal):
 1. esize s < enat (Suc k) \<Longrightarrow> w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w ?! i = w ?! nth_least_ext s k

goal (1 subgoal):
 1. w ?! i = w ?! nth_least_ext s k
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
w ?! i = w ?! nth_least_ext s k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
w ?! i = w ?! nth_least_ext s k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stutter_equivI_selection[intro]:
    assumes "linfinite u" "linfinite v"
    assumes "stutter_selection s u" "stutter_selection t v"
    assumes "lselect s u = lselect t v"
    shows "lnth u \<approx> lnth v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (?!) u \<approx> (?!) v
[PROOF STEP]
proof (rule stutter_equivI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. stutter_sampler ?f ((?!) u)
 2. stutter_sampler ?g ((?!) v)
 3. (?!) u \<circ> ?f = (?!) v \<circ> ?g
[PROOF STEP]
have 1: "llength (lselect s u) = llength (lselect t v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llength (lselect s u) = llength (lselect t v)
[PROOF STEP]
unfolding assms(5)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llength (lselect t v) = llength (lselect t v)
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
llength (lselect s u) = llength (lselect t v)

goal (3 subgoals):
 1. stutter_sampler ?f ((?!) u)
 2. stutter_sampler ?g ((?!) v)
 3. (?!) u \<circ> ?f = (?!) v \<circ> ?g
[PROOF STEP]
have 2: "esize s = esize t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. esize s = esize t
[PROOF STEP]
using 1 assms(1, 2)
[PROOF STATE]
proof (prove)
using this:
llength (lselect s u) = llength (lselect t v)
linfinite u
linfinite v

goal (1 subgoal):
 1. esize s = esize t
[PROOF STEP]
unfolding lselect_llength
[PROOF STATE]
proof (prove)
using this:
esize {i \<in> s. enat i < llength u} = esize {i \<in> t. enat i < llength v}
linfinite u
linfinite v

goal (1 subgoal):
 1. esize s = esize t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
esize s = esize t

goal (3 subgoals):
 1. stutter_sampler ?f ((?!) u)
 2. stutter_sampler ?g ((?!) v)
 3. (?!) u \<circ> ?f = (?!) v \<circ> ?g
[PROOF STEP]
show "stutter_sampler (nth_least_ext s) (lnth u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_sampler (nth_least_ext s) ((?!) u)
[PROOF STEP]
using assms(1, 3)
[PROOF STATE]
proof (prove)
using this:
linfinite u
stutter_selection s u

goal (1 subgoal):
 1. stutter_sampler (nth_least_ext s) ((?!) u)
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
stutter_sampler (nth_least_ext s) ((?!) u)

goal (2 subgoals):
 1. stutter_sampler ?g ((?!) v)
 2. (?!) u \<circ> nth_least_ext s = (?!) v \<circ> ?g
[PROOF STEP]
show "stutter_sampler (nth_least_ext t) (lnth v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_sampler (nth_least_ext t) ((?!) v)
[PROOF STEP]
using assms(2, 4)
[PROOF STATE]
proof (prove)
using this:
linfinite v
stutter_selection t v

goal (1 subgoal):
 1. stutter_sampler (nth_least_ext t) ((?!) v)
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
stutter_sampler (nth_least_ext t) ((?!) v)

goal (1 subgoal):
 1. (?!) u \<circ> nth_least_ext s = (?!) v \<circ> nth_least_ext t
[PROOF STEP]
show "lnth u \<circ> nth_least_ext s = lnth v \<circ> nth_least_ext t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (?!) u \<circ> nth_least_ext s = (?!) v \<circ> nth_least_ext t
[PROOF STEP]
proof (rule ext, unfold comp_apply)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. u ?! nth_least_ext s x = v ?! nth_least_ext t x
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. u ?! nth_least_ext s x = v ?! nth_least_ext t x
[PROOF STEP]
show "u ?! nth_least_ext s i = v ?! nth_least_ext t i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
proof (cases "enat i < esize s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
 2. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
enat i < esize s

goal (2 subgoals):
 1. enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
 2. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have 3: "enat i < llength (lselect s u)" "enat i < llength (lselect t v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat i < llength (lselect s u) &&& enat i < llength (lselect t v)
[PROOF STEP]
using assms(1, 2) 2 True
[PROOF STATE]
proof (prove)
using this:
linfinite u
linfinite v
esize s = esize t
enat i < esize s

goal (1 subgoal):
 1. enat i < llength (lselect s u) &&& enat i < llength (lselect t v)
[PROOF STEP]
unfolding lselect_llength
[PROOF STATE]
proof (prove)
using this:
linfinite u
linfinite v
esize s = esize t
enat i < esize s

goal (1 subgoal):
 1. enat i < esize {i \<in> s. enat i < llength u} &&& enat i < esize {i \<in> t. enat i < llength v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enat i < llength (lselect s u)
enat i < llength (lselect t v)

goal (2 subgoals):
 1. enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
 2. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "u ?! nth_least_ext s i = u ?! nth_least s i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u ?! nth_least_ext s i = u ?! nth_least s i
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
enat i < esize s

goal (1 subgoal):
 1. u ?! nth_least_ext s i = u ?! nth_least s i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u ?! nth_least_ext s i = u ?! nth_least s i

goal (2 subgoals):
 1. enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
 2. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u ?! nth_least_ext s i = u ?! nth_least s i

goal (2 subgoals):
 1. enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
 2. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "\<dots> = lselect s u ?! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u ?! nth_least s i = lselect s u ?! i
[PROOF STEP]
using 3(1)
[PROOF STATE]
proof (prove)
using this:
enat i < llength (lselect s u)

goal (1 subgoal):
 1. u ?! nth_least s i = lselect s u ?! i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u ?! nth_least s i = lselect s u ?! i

goal (2 subgoals):
 1. enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
 2. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u ?! nth_least s i = lselect s u ?! i

goal (2 subgoals):
 1. enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
 2. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "\<dots> = lselect t v ?! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lselect s u ?! i = lselect t v ?! i
[PROOF STEP]
unfolding assms(5)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lselect t v ?! i = lselect t v ?! i
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
lselect s u ?! i = lselect t v ?! i

goal (2 subgoals):
 1. enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
 2. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lselect s u ?! i = lselect t v ?! i

goal (2 subgoals):
 1. enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
 2. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "\<dots> = v ?! nth_least t i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lselect t v ?! i = v ?! nth_least t i
[PROOF STEP]
using 3(2)
[PROOF STATE]
proof (prove)
using this:
enat i < llength (lselect t v)

goal (1 subgoal):
 1. lselect t v ?! i = v ?! nth_least t i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lselect t v ?! i = v ?! nth_least t i

goal (2 subgoals):
 1. enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
 2. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lselect t v ?! i = v ?! nth_least t i

goal (2 subgoals):
 1. enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
 2. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "\<dots> = v ?! nth_least_ext t i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v ?! nth_least t i = v ?! nth_least_ext t i
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
enat i < esize s

goal (1 subgoal):
 1. v ?! nth_least t i = v ?! nth_least_ext t i
[PROOF STEP]
unfolding 2
[PROOF STATE]
proof (prove)
using this:
enat i < esize t

goal (1 subgoal):
 1. v ?! nth_least t i = v ?! nth_least_ext t i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v ?! nth_least t i = v ?! nth_least_ext t i

goal (2 subgoals):
 1. enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
 2. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
show "u ?! nth_least_ext s i = v ?! nth_least_ext t i"
[PROOF STATE]
proof (prove)
using this:
u ?! nth_least_ext s i = v ?! nth_least_ext t i

goal (1 subgoal):
 1. u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
u ?! nth_least_ext s i = v ?! nth_least_ext t i

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> enat i < esize s

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have 3: "s \<noteq> {}" "t \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> {} &&& t \<noteq> {}
[PROOF STEP]
using assms(3, 4)
[PROOF STATE]
proof (prove)
using this:
stutter_selection s u
stutter_selection t v

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

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have 4: "finite s" "finite t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite s &&& finite t
[PROOF STEP]
using esize_infinite_enat 2 False
[PROOF STATE]
proof (prove)
using this:
infinite ?A \<Longrightarrow> enat ?k < esize ?A
esize s = esize t
\<not> enat i < esize s

goal (1 subgoal):
 1. finite s &&& finite t
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
finite s
finite t

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have 5: "\<And> i. i > Max s \<Longrightarrow> u ?! i = u ?! Max s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. Max s < i \<Longrightarrow> u ?! i = u ?! Max s
[PROOF STEP]
using assms(1, 3) 4(1)
[PROOF STATE]
proof (prove)
using this:
linfinite u
stutter_selection s u
finite s

goal (1 subgoal):
 1. \<And>i. Max s < i \<Longrightarrow> u ?! i = u ?! Max s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max s < ?i \<Longrightarrow> u ?! ?i = u ?! Max s

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have 6: "\<And> i. i > Max t \<Longrightarrow> v ?! i = v ?! Max t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. Max t < i \<Longrightarrow> v ?! i = v ?! Max t
[PROOF STEP]
using assms(2, 4) 4(2)
[PROOF STATE]
proof (prove)
using this:
linfinite v
stutter_selection t v
finite t

goal (1 subgoal):
 1. \<And>i. Max t < i \<Longrightarrow> v ?! i = v ?! Max t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max t < ?i \<Longrightarrow> v ?! ?i = v ?! Max t

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have 7: "esize s = enat (card s)" "esize t = enat (card t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. esize s = enat (card s) &&& esize t = enat (card t)
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
finite s
finite t

goal (1 subgoal):
 1. esize s = enat (card s) &&& esize t = enat (card t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
esize s = enat (card s)
esize t = enat (card t)

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have 8: "card s \<noteq> 0" "card t \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card s \<noteq> 0 &&& card t \<noteq> 0
[PROOF STEP]
using 3 4
[PROOF STATE]
proof (prove)
using this:
s \<noteq> {}
t \<noteq> {}
finite s
finite t

goal (1 subgoal):
 1. card s \<noteq> 0 &&& card t \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card s \<noteq> 0
card t \<noteq> 0

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have 9: "enat (card s - 1) < llength (lselect s u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat (card s - 1) < llength (lselect s u)
[PROOF STEP]
using assms(1) 7(1) 8(1)
[PROOF STATE]
proof (prove)
using this:
linfinite u
esize s = enat (card s)
card s \<noteq> 0

goal (1 subgoal):
 1. enat (card s - 1) < llength (lselect s u)
[PROOF STEP]
unfolding lselect_llength
[PROOF STATE]
proof (prove)
using this:
linfinite u
esize s = enat (card s)
card s \<noteq> 0

goal (1 subgoal):
 1. enat (card s - 1) < esize {i \<in> s. enat i < llength u}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enat (card s - 1) < llength (lselect s u)

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have 10: "enat (card t - 1) < llength (lselect t v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat (card t - 1) < llength (lselect t v)
[PROOF STEP]
using assms(2) 7(2) 8(2)
[PROOF STATE]
proof (prove)
using this:
linfinite v
esize t = enat (card t)
card t \<noteq> 0

goal (1 subgoal):
 1. enat (card t - 1) < llength (lselect t v)
[PROOF STEP]
unfolding lselect_llength
[PROOF STATE]
proof (prove)
using this:
linfinite v
esize t = enat (card t)
card t \<noteq> 0

goal (1 subgoal):
 1. enat (card t - 1) < esize {i \<in> t. enat i < llength v}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enat (card t - 1) < llength (lselect t v)

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "u ?! nth_least_ext s i = u ?! Suc (Max s + (i - card s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u ?! nth_least_ext s i = u ?! Suc (Max s + (i - card s))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> enat i < esize s

goal (1 subgoal):
 1. u ?! nth_least_ext s i = u ?! Suc (Max s + (i - card s))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u ?! nth_least_ext s i = u ?! Suc (Max s + (i - card s))

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u ?! nth_least_ext s i = u ?! Suc (Max s + (i - card s))

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "\<dots> = u ?! Max s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u ?! Suc (Max s + (i - card s)) = u ?! Max s
[PROOF STEP]
using 5
[PROOF STATE]
proof (prove)
using this:
Max s < ?i \<Longrightarrow> u ?! ?i = u ?! Max s

goal (1 subgoal):
 1. u ?! Suc (Max s + (i - card s)) = u ?! Max s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u ?! Suc (Max s + (i - card s)) = u ?! Max s

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u ?! Suc (Max s + (i - card s)) = u ?! Max s

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "\<dots> = u ?! nth_least s (card s - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u ?! Max s = u ?! nth_least s (card s - 1)
[PROOF STEP]
using nth_least_Max 4(1) 3(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> nth_least ?A (card ?A - 1) = Max ?A
finite s
s \<noteq> {}

goal (1 subgoal):
 1. u ?! Max s = u ?! nth_least s (card s - 1)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
u ?! Max s = u ?! nth_least s (card s - 1)

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u ?! Max s = u ?! nth_least s (card s - 1)

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "\<dots> = lselect s u ?! (card s - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u ?! nth_least s (card s - 1) = lselect s u ?! (card s - 1)
[PROOF STEP]
using lselect_lnth 9
[PROOF STATE]
proof (prove)
using this:
enat ?i < llength (lselect ?s ?w) \<Longrightarrow> lselect ?s ?w ?! ?i = ?w ?! nth_least ?s ?i
enat (card s - 1) < llength (lselect s u)

goal (1 subgoal):
 1. u ?! nth_least s (card s - 1) = lselect s u ?! (card s - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u ?! nth_least s (card s - 1) = lselect s u ?! (card s - 1)

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u ?! nth_least s (card s - 1) = lselect s u ?! (card s - 1)

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "\<dots> = lselect s u ?! (card t - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lselect s u ?! (card s - 1) = lselect s u ?! (card t - 1)
[PROOF STEP]
using 2 4
[PROOF STATE]
proof (prove)
using this:
esize s = esize t
finite s
finite t

goal (1 subgoal):
 1. lselect s u ?! (card s - 1) = lselect s u ?! (card t - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lselect s u ?! (card s - 1) = lselect s u ?! (card t - 1)

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lselect s u ?! (card s - 1) = lselect s u ?! (card t - 1)

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "\<dots> = lselect t v ?! (card t - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lselect s u ?! (card t - 1) = lselect t v ?! (card t - 1)
[PROOF STEP]
unfolding assms(5)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lselect t v ?! (card t - 1) = lselect t v ?! (card t - 1)
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
lselect s u ?! (card t - 1) = lselect t v ?! (card t - 1)

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lselect s u ?! (card t - 1) = lselect t v ?! (card t - 1)

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "\<dots> = v ?! nth_least t (card t - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lselect t v ?! (card t - 1) = v ?! nth_least t (card t - 1)
[PROOF STEP]
using lselect_lnth 10
[PROOF STATE]
proof (prove)
using this:
enat ?i < llength (lselect ?s ?w) \<Longrightarrow> lselect ?s ?w ?! ?i = ?w ?! nth_least ?s ?i
enat (card t - 1) < llength (lselect t v)

goal (1 subgoal):
 1. lselect t v ?! (card t - 1) = v ?! nth_least t (card t - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lselect t v ?! (card t - 1) = v ?! nth_least t (card t - 1)

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lselect t v ?! (card t - 1) = v ?! nth_least t (card t - 1)

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "\<dots> = v ?! Max t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v ?! nth_least t (card t - 1) = v ?! Max t
[PROOF STEP]
using nth_least_Max 4(2) 3(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> nth_least ?A (card ?A - 1) = Max ?A
finite t
t \<noteq> {}

goal (1 subgoal):
 1. v ?! nth_least t (card t - 1) = v ?! Max t
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
v ?! nth_least t (card t - 1) = v ?! Max t

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
v ?! nth_least t (card t - 1) = v ?! Max t

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "\<dots> = v ?! Suc (Max t + (i - card t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v ?! Max t = v ?! Suc (Max t + (i - card t))
[PROOF STEP]
using 6
[PROOF STATE]
proof (prove)
using this:
Max t < ?i \<Longrightarrow> v ?! ?i = v ?! Max t

goal (1 subgoal):
 1. v ?! Max t = v ?! Suc (Max t + (i - card t))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v ?! Max t = v ?! Suc (Max t + (i - card t))

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
v ?! Max t = v ?! Suc (Max t + (i - card t))

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
have "\<dots> = v ?! nth_least_ext t i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v ?! Suc (Max t + (i - card t)) = v ?! nth_least_ext t i
[PROOF STEP]
using 2 False
[PROOF STATE]
proof (prove)
using this:
esize s = esize t
\<not> enat i < esize s

goal (1 subgoal):
 1. v ?! Suc (Max t + (i - card t)) = v ?! nth_least_ext t i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v ?! Suc (Max t + (i - card t)) = v ?! nth_least_ext t i

goal (1 subgoal):
 1. \<not> enat i < esize s \<Longrightarrow> u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u ?! nth_least_ext s i = v ?! nth_least_ext t i

goal (1 subgoal):
 1. u ?! nth_least_ext s i = v ?! nth_least_ext t i
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
u ?! nth_least_ext s i = v ?! nth_least_ext t i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u ?! nth_least_ext s i = v ?! nth_least_ext t i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?!) u \<circ> nth_least_ext s = (?!) v \<circ> nth_least_ext t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stuttering_invariant_complement[intro!]:
    assumes "stuttering_invariant A"
    shows "stuttering_invariant (- A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stuttering_invariant (- A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
stuttering_invariant A

goal (1 subgoal):
 1. stuttering_invariant (- A)
[PROOF STEP]
unfolding stuttering_invariant_def
[PROOF STATE]
proof (prove)
using this:
\<forall>u v. u \<approx> v \<longrightarrow> (u \<in> A) = (v \<in> A)

goal (1 subgoal):
 1. \<forall>u v. u \<approx> v \<longrightarrow> (u \<in> - A) = (v \<in> - A)
[PROOF STEP]
by simp


[STATEMENT]
lemma stutter_equiv_forw_subst[trans]: "w\<^sub>1 = w\<^sub>2 \<Longrightarrow> w\<^sub>2 \<approx> w\<^sub>3 \<Longrightarrow> w\<^sub>1 \<approx> w\<^sub>3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w\<^sub>1 = w\<^sub>2; w\<^sub>2 \<approx> w\<^sub>3\<rbrakk> \<Longrightarrow> w\<^sub>1 \<approx> w\<^sub>3
[PROOF STEP]
by auto


[STATEMENT]
lemma stutter_sampler_build:
    assumes "stutter_sampler f w"
    shows "stutter_sampler (0 ## (Suc \<circ> f)) (a ## w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_sampler (0 ## (Suc \<circ> f)) (a ## w)
[PROOF STEP]
unfolding stutter_sampler_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 ## (Suc \<circ> f)) 0 = 0 \<and> strict_mono (0 ## (Suc \<circ> f)) \<and> (\<forall>k n. (0 ## (Suc \<circ> f)) k < n \<and> n < (0 ## (Suc \<circ> f)) (Suc k) \<longrightarrow> (a ## w) n = (a ## w) ((0 ## (Suc \<circ> f)) k))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (0 ## (Suc \<circ> f)) 0 = 0
 2. strict_mono (0 ## (Suc \<circ> f))
 3. \<And>k n. \<lbrakk>(0 ## (Suc \<circ> f)) k < n; n < (0 ## (Suc \<circ> f)) (Suc k)\<rbrakk> \<Longrightarrow> (a ## w) n = (a ## w) ((0 ## (Suc \<circ> f)) k)
[PROOF STEP]
have 0: "f 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f 0 = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
stutter_sampler f w

goal (1 subgoal):
 1. f 0 = 0
[PROOF STEP]
unfolding stutter_sampler_def
[PROOF STATE]
proof (prove)
using this:
f 0 = 0 \<and> strict_mono f \<and> (\<forall>k n. f k < n \<and> n < f (Suc k) \<longrightarrow> w n = w (f k))

goal (1 subgoal):
 1. f 0 = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f 0 = 0

goal (3 subgoals):
 1. (0 ## (Suc \<circ> f)) 0 = 0
 2. strict_mono (0 ## (Suc \<circ> f))
 3. \<And>k n. \<lbrakk>(0 ## (Suc \<circ> f)) k < n; n < (0 ## (Suc \<circ> f)) (Suc k)\<rbrakk> \<Longrightarrow> (a ## w) n = (a ## w) ((0 ## (Suc \<circ> f)) k)
[PROOF STEP]
have 1: "f x < f y" if "x < y" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x < f y
[PROOF STEP]
using assms that
[PROOF STATE]
proof (prove)
using this:
stutter_sampler f w
x < y

goal (1 subgoal):
 1. f x < f y
[PROOF STEP]
unfolding stutter_sampler_def strict_mono_def
[PROOF STATE]
proof (prove)
using this:
f 0 = 0 \<and> (\<forall>x y. x < y \<longrightarrow> f x < f y) \<and> (\<forall>k n. f k < n \<and> n < f (Suc k) \<longrightarrow> w n = w (f k))
x < y

goal (1 subgoal):
 1. f x < f y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x < ?y \<Longrightarrow> f ?x < f ?y

goal (3 subgoals):
 1. (0 ## (Suc \<circ> f)) 0 = 0
 2. strict_mono (0 ## (Suc \<circ> f))
 3. \<And>k n. \<lbrakk>(0 ## (Suc \<circ> f)) k < n; n < (0 ## (Suc \<circ> f)) (Suc k)\<rbrakk> \<Longrightarrow> (a ## w) n = (a ## w) ((0 ## (Suc \<circ> f)) k)
[PROOF STEP]
have 2: "(0 ## (Suc \<circ> f)) x < (0 ## (Suc \<circ> f)) y" if "x < y" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 ## (Suc \<circ> f)) x < (0 ## (Suc \<circ> f)) y
[PROOF STEP]
using 1 that
[PROOF STATE]
proof (prove)
using this:
?x < ?y \<Longrightarrow> f ?x < f ?y
x < y

goal (1 subgoal):
 1. (0 ## (Suc \<circ> f)) x < (0 ## (Suc \<circ> f)) y
[PROOF STEP]
by (cases x; cases y) (auto)
[PROOF STATE]
proof (state)
this:
?x < ?y \<Longrightarrow> (0 ## (Suc \<circ> f)) ?x < (0 ## (Suc \<circ> f)) ?y

goal (3 subgoals):
 1. (0 ## (Suc \<circ> f)) 0 = 0
 2. strict_mono (0 ## (Suc \<circ> f))
 3. \<And>k n. \<lbrakk>(0 ## (Suc \<circ> f)) k < n; n < (0 ## (Suc \<circ> f)) (Suc k)\<rbrakk> \<Longrightarrow> (a ## w) n = (a ## w) ((0 ## (Suc \<circ> f)) k)
[PROOF STEP]
have 3: "w n = w (f k)" if "f k < n" "n < f (Suc k)" for k n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w n = w (f k)
[PROOF STEP]
using assms that
[PROOF STATE]
proof (prove)
using this:
stutter_sampler f w
f k < n
n < f (Suc k)

goal (1 subgoal):
 1. w n = w (f k)
[PROOF STEP]
unfolding stutter_sampler_def
[PROOF STATE]
proof (prove)
using this:
f 0 = 0 \<and> strict_mono f \<and> (\<forall>k n. f k < n \<and> n < f (Suc k) \<longrightarrow> w n = w (f k))
f k < n
n < f (Suc k)

goal (1 subgoal):
 1. w n = w (f k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>f ?k < ?n; ?n < f (Suc ?k)\<rbrakk> \<Longrightarrow> w ?n = w (f ?k)

goal (3 subgoals):
 1. (0 ## (Suc \<circ> f)) 0 = 0
 2. strict_mono (0 ## (Suc \<circ> f))
 3. \<And>k n. \<lbrakk>(0 ## (Suc \<circ> f)) k < n; n < (0 ## (Suc \<circ> f)) (Suc k)\<rbrakk> \<Longrightarrow> (a ## w) n = (a ## w) ((0 ## (Suc \<circ> f)) k)
[PROOF STEP]
show "(0 ## (Suc \<circ> f)) 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 ## (Suc \<circ> f)) 0 = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0 ## (Suc \<circ> f)) 0 = 0

goal (2 subgoals):
 1. strict_mono (0 ## (Suc \<circ> f))
 2. \<And>k n. \<lbrakk>(0 ## (Suc \<circ> f)) k < n; n < (0 ## (Suc \<circ> f)) (Suc k)\<rbrakk> \<Longrightarrow> (a ## w) n = (a ## w) ((0 ## (Suc \<circ> f)) k)
[PROOF STEP]
show "strict_mono (0 ## (Suc \<circ> f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_mono (0 ## (Suc \<circ> f))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
?x < ?y \<Longrightarrow> (0 ## (Suc \<circ> f)) ?x < (0 ## (Suc \<circ> f)) ?y

goal (1 subgoal):
 1. strict_mono (0 ## (Suc \<circ> f))
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
strict_mono (0 ## (Suc \<circ> f))

goal (1 subgoal):
 1. \<And>k n. \<lbrakk>(0 ## (Suc \<circ> f)) k < n; n < (0 ## (Suc \<circ> f)) (Suc k)\<rbrakk> \<Longrightarrow> (a ## w) n = (a ## w) ((0 ## (Suc \<circ> f)) k)
[PROOF STEP]
show "(a ## w) n = (a ## w) ((0 ## (Suc \<circ> f)) k)"
      if "(0 ## (Suc \<circ> f)) k < n" "n < (0 ## (Suc \<circ> f)) (Suc k)" for k n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a ## w) n = (a ## w) ((0 ## (Suc \<circ> f)) k)
[PROOF STEP]
using 0 3 that
[PROOF STATE]
proof (prove)
using this:
f 0 = 0
\<lbrakk>f ?k < ?n; ?n < f (Suc ?k)\<rbrakk> \<Longrightarrow> w ?n = w (f ?k)
(0 ## (Suc \<circ> f)) k < n
n < (0 ## (Suc \<circ> f)) (Suc k)

goal (1 subgoal):
 1. (a ## w) n = (a ## w) ((0 ## (Suc \<circ> f)) k)
[PROOF STEP]
by (cases k; cases n) (force)+
[PROOF STATE]
proof (state)
this:
\<lbrakk>(0 ## (Suc \<circ> f)) ?k < ?n; ?n < (0 ## (Suc \<circ> f)) (Suc ?k)\<rbrakk> \<Longrightarrow> (a ## w) ?n = (a ## w) ((0 ## (Suc \<circ> f)) ?k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stutter_extend_build:
    assumes "u \<approx> v"
    shows "a ## u \<approx> a ## v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ## u \<approx> a ## v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a ## u \<approx> a ## v
[PROOF STEP]
obtain f g where 1: "stutter_sampler f u" "stutter_sampler g v" "u \<circ> f = v \<circ> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f g. \<lbrakk>stutter_sampler f u; stutter_sampler g v; u \<circ> f = v \<circ> g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using stutter_equivE assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<sigma> \<approx> ?\<tau>; \<And>f g. \<lbrakk>stutter_sampler f ?\<sigma>; stutter_sampler g ?\<tau>; ?\<sigma> \<circ> f = ?\<tau> \<circ> g\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
u \<approx> v

goal (1 subgoal):
 1. (\<And>f g. \<lbrakk>stutter_sampler f u; stutter_sampler g v; u \<circ> f = v \<circ> g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
stutter_sampler f u
stutter_sampler g v
u \<circ> f = v \<circ> g

goal (1 subgoal):
 1. a ## u \<approx> a ## v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ## u \<approx> a ## v
[PROOF STEP]
proof (intro stutter_equivI ext)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. stutter_sampler ?f (a ## u)
 2. stutter_sampler ?g (a ## v)
 3. \<And>x. (a ## u \<circ> ?f) x = (a ## v \<circ> ?g) x
[PROOF STEP]
show "stutter_sampler (0 ## (Suc \<circ> f)) (a ## u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_sampler (0 ## (Suc \<circ> f)) (a ## u)
[PROOF STEP]
using stutter_sampler_build 1(1)
[PROOF STATE]
proof (prove)
using this:
stutter_sampler ?f ?w \<Longrightarrow> stutter_sampler (0 ## (Suc \<circ> ?f)) (?a ## ?w)
stutter_sampler f u

goal (1 subgoal):
 1. stutter_sampler (0 ## (Suc \<circ> f)) (a ## u)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
stutter_sampler (0 ## (Suc \<circ> f)) (a ## u)

goal (2 subgoals):
 1. stutter_sampler ?g (a ## v)
 2. \<And>x. (a ## u \<circ> 0 ## (Suc \<circ> f)) x = (a ## v \<circ> ?g) x
[PROOF STEP]
show "stutter_sampler (0 ## (Suc \<circ> g)) (a ## v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_sampler (0 ## (Suc \<circ> g)) (a ## v)
[PROOF STEP]
using stutter_sampler_build 1(2)
[PROOF STATE]
proof (prove)
using this:
stutter_sampler ?f ?w \<Longrightarrow> stutter_sampler (0 ## (Suc \<circ> ?f)) (?a ## ?w)
stutter_sampler g v

goal (1 subgoal):
 1. stutter_sampler (0 ## (Suc \<circ> g)) (a ## v)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
stutter_sampler (0 ## (Suc \<circ> g)) (a ## v)

goal (1 subgoal):
 1. \<And>x. (a ## u \<circ> 0 ## (Suc \<circ> f)) x = (a ## v \<circ> 0 ## (Suc \<circ> g)) x
[PROOF STEP]
show "(a ## u \<circ> 0 ## (Suc \<circ> f)) i = (a ## v \<circ> 0 ## (Suc \<circ> g)) i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a ## u \<circ> 0 ## (Suc \<circ> f)) i = (a ## v \<circ> 0 ## (Suc \<circ> g)) i
[PROOF STEP]
using fun_cong[OF 1(3)]
[PROOF STATE]
proof (prove)
using this:
(u \<circ> f) ?x = (v \<circ> g) ?x

goal (1 subgoal):
 1. (a ## u \<circ> 0 ## (Suc \<circ> f)) i = (a ## v \<circ> 0 ## (Suc \<circ> g)) i
[PROOF STEP]
by (cases i) (auto)
[PROOF STATE]
proof (state)
this:
(a ## u \<circ> 0 ## (Suc \<circ> f)) ?i = (a ## v \<circ> 0 ## (Suc \<circ> g)) ?i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a ## u \<approx> a ## v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stutter_extend_concat:
    assumes "u \<approx> v"
    shows "w \<frown> u \<approx> w \<frown> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<frown> u \<approx> w \<frown> v
[PROOF STEP]
using stutter_extend_build assms
[PROOF STATE]
proof (prove)
using this:
?u \<approx> ?v \<Longrightarrow> ?a ## ?u \<approx> ?a ## ?v
u \<approx> v

goal (1 subgoal):
 1. w \<frown> u \<approx> w \<frown> v
[PROOF STEP]
by (induct w, force+)


[STATEMENT]
lemma build_stutter: "w 0 ## w \<approx> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w 0 ## w \<approx> w
[PROOF STEP]
proof (rule stutter_equivI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. stutter_sampler ?f (w 0 ## w)
 2. stutter_sampler ?g w
 3. w 0 ## w \<circ> ?f = w \<circ> ?g
[PROOF STEP]
show "stutter_sampler (Suc (0 := 0)) (w 0 ## w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_sampler (Suc(0 := 0)) (w 0 ## w)
[PROOF STEP]
unfolding stutter_sampler_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Suc(0 := 0)) 0 = 0 \<and> strict_mono (Suc(0 := 0)) \<and> (\<forall>k n. (Suc(0 := 0)) k < n \<and> n < (Suc(0 := 0)) (Suc k) \<longrightarrow> (w 0 ## w) n = (w 0 ## w) ((Suc(0 := 0)) k))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (Suc(0 := 0)) 0 = 0
 2. strict_mono (Suc(0 := 0))
 3. \<And>k n. \<lbrakk>(Suc(0 := 0)) k < n; n < (Suc(0 := 0)) (Suc k)\<rbrakk> \<Longrightarrow> (w 0 ## w) n = (w 0 ## w) ((Suc(0 := 0)) k)
[PROOF STEP]
show "(Suc (0 := 0)) 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Suc(0 := 0)) 0 = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(Suc(0 := 0)) 0 = 0

goal (2 subgoals):
 1. strict_mono (Suc(0 := 0))
 2. \<And>k n. \<lbrakk>(Suc(0 := 0)) k < n; n < (Suc(0 := 0)) (Suc k)\<rbrakk> \<Longrightarrow> (w 0 ## w) n = (w 0 ## w) ((Suc(0 := 0)) k)
[PROOF STEP]
show "strict_mono (Suc (0 := 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_mono (Suc(0 := 0))
[PROOF STEP]
by (rule strict_monoI, simp)
[PROOF STATE]
proof (state)
this:
strict_mono (Suc(0 := 0))

goal (1 subgoal):
 1. \<And>k n. \<lbrakk>(Suc(0 := 0)) k < n; n < (Suc(0 := 0)) (Suc k)\<rbrakk> \<Longrightarrow> (w 0 ## w) n = (w 0 ## w) ((Suc(0 := 0)) k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k n. \<lbrakk>(Suc(0 := 0)) k < n; n < (Suc(0 := 0)) (Suc k)\<rbrakk> \<Longrightarrow> (w 0 ## w) n = (w 0 ## w) ((Suc(0 := 0)) k)
[PROOF STEP]
fix k n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k n. \<lbrakk>(Suc(0 := 0)) k < n; n < (Suc(0 := 0)) (Suc k)\<rbrakk> \<Longrightarrow> (w 0 ## w) n = (w 0 ## w) ((Suc(0 := 0)) k)
[PROOF STEP]
assume 1: "(Suc (0 := 0)) k < n" "n < (Suc (0 := 0)) (Suc k)"
[PROOF STATE]
proof (state)
this:
(Suc(0 := 0)) k < n
n < (Suc(0 := 0)) (Suc k)

goal (1 subgoal):
 1. \<And>k n. \<lbrakk>(Suc(0 := 0)) k < n; n < (Suc(0 := 0)) (Suc k)\<rbrakk> \<Longrightarrow> (w 0 ## w) n = (w 0 ## w) ((Suc(0 := 0)) k)
[PROOF STEP]
show "(w 0 ## w) n = (w 0 ## w) ((Suc (0 := 0)) k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w 0 ## w) n = (w 0 ## w) ((Suc(0 := 0)) k)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
(Suc(0 := 0)) k < n
n < (Suc(0 := 0)) (Suc k)

goal (1 subgoal):
 1. (w 0 ## w) n = (w 0 ## w) ((Suc(0 := 0)) k)
[PROOF STEP]
by (cases n, auto)
[PROOF STATE]
proof (state)
this:
(w 0 ## w) n = (w 0 ## w) ((Suc(0 := 0)) k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
stutter_sampler (Suc(0 := 0)) (w 0 ## w)

goal (2 subgoals):
 1. stutter_sampler ?g w
 2. w 0 ## w \<circ> Suc(0 := 0) = w \<circ> ?g
[PROOF STEP]
show "stutter_sampler id w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_sampler id w
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
stutter_sampler id w

goal (1 subgoal):
 1. w 0 ## w \<circ> Suc(0 := 0) = w \<circ> id
[PROOF STEP]
show "w 0 ## w \<circ> (Suc (0 := 0)) = w \<circ> id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w 0 ## w \<circ> Suc(0 := 0) = w \<circ> id
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w 0 ## w \<circ> Suc(0 := 0) = w \<circ> id

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma replicate_stutter: "replicate n (v 0) \<frown> v \<approx> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. replicate n (v 0) \<frown> v \<approx> v
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. replicate 0 (v 0) \<frown> v \<approx> v
 2. \<And>n. replicate n (v 0) \<frown> v \<approx> v \<Longrightarrow> replicate (Suc n) (v 0) \<frown> v \<approx> v
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. replicate 0 (v 0) \<frown> v \<approx> v
 2. \<And>n. replicate n (v 0) \<frown> v \<approx> v \<Longrightarrow> replicate (Suc n) (v 0) \<frown> v \<approx> v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. replicate 0 (v 0) \<frown> v \<approx> v
[PROOF STEP]
using stutter_equiv_refl
[PROOF STATE]
proof (prove)
using this:
?\<sigma> \<approx> ?\<sigma>

goal (1 subgoal):
 1. replicate 0 (v 0) \<frown> v \<approx> v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
replicate 0 (v 0) \<frown> v \<approx> v

goal (1 subgoal):
 1. \<And>n. replicate n (v 0) \<frown> v \<approx> v \<Longrightarrow> replicate (Suc n) (v 0) \<frown> v \<approx> v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. replicate n (v 0) \<frown> v \<approx> v \<Longrightarrow> replicate (Suc n) (v 0) \<frown> v \<approx> v
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
replicate n (v 0) \<frown> v \<approx> v

goal (1 subgoal):
 1. \<And>n. replicate n (v 0) \<frown> v \<approx> v \<Longrightarrow> replicate (Suc n) (v 0) \<frown> v \<approx> v
[PROOF STEP]
have "replicate (Suc n) (v 0) \<frown> v = v 0 ## replicate n (v 0) \<frown> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. replicate (Suc n) (v 0) \<frown> v = v 0 ## replicate n (v 0) \<frown> v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
replicate (Suc n) (v 0) \<frown> v = v 0 ## replicate n (v 0) \<frown> v

goal (1 subgoal):
 1. \<And>n. replicate n (v 0) \<frown> v \<approx> v \<Longrightarrow> replicate (Suc n) (v 0) \<frown> v \<approx> v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
replicate (Suc n) (v 0) \<frown> v = v 0 ## replicate n (v 0) \<frown> v

goal (1 subgoal):
 1. \<And>n. replicate n (v 0) \<frown> v \<approx> v \<Longrightarrow> replicate (Suc n) (v 0) \<frown> v \<approx> v
[PROOF STEP]
have "\<dots> = (replicate n (v 0) \<frown> v) 0 ## replicate n (v 0) \<frown> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v 0 ## replicate n (v 0) \<frown> v = (replicate n (v 0) \<frown> v) 0 ## replicate n (v 0) \<frown> v
[PROOF STEP]
by (cases n, auto)
[PROOF STATE]
proof (state)
this:
v 0 ## replicate n (v 0) \<frown> v = (replicate n (v 0) \<frown> v) 0 ## replicate n (v 0) \<frown> v

goal (1 subgoal):
 1. \<And>n. replicate n (v 0) \<frown> v \<approx> v \<Longrightarrow> replicate (Suc n) (v 0) \<frown> v \<approx> v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
v 0 ## replicate n (v 0) \<frown> v = (replicate n (v 0) \<frown> v) 0 ## replicate n (v 0) \<frown> v

goal (1 subgoal):
 1. \<And>n. replicate n (v 0) \<frown> v \<approx> v \<Longrightarrow> replicate (Suc n) (v 0) \<frown> v \<approx> v
[PROOF STEP]
have "\<dots> \<approx> replicate n (v 0) \<frown> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (replicate n (v 0) \<frown> v) 0 ## replicate n (v 0) \<frown> v \<approx> replicate n (v 0) \<frown> v
[PROOF STEP]
using build_stutter
[PROOF STATE]
proof (prove)
using this:
?w 0 ## ?w \<approx> ?w

goal (1 subgoal):
 1. (replicate n (v 0) \<frown> v) 0 ## replicate n (v 0) \<frown> v \<approx> replicate n (v 0) \<frown> v
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
(replicate n (v 0) \<frown> v) 0 ## replicate n (v 0) \<frown> v \<approx> replicate n (v 0) \<frown> v

goal (1 subgoal):
 1. \<And>n. replicate n (v 0) \<frown> v \<approx> v \<Longrightarrow> replicate (Suc n) (v 0) \<frown> v \<approx> v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(replicate n (v 0) \<frown> v) 0 ## replicate n (v 0) \<frown> v \<approx> replicate n (v 0) \<frown> v

goal (1 subgoal):
 1. \<And>n. replicate n (v 0) \<frown> v \<approx> v \<Longrightarrow> replicate (Suc n) (v 0) \<frown> v \<approx> v
[PROOF STEP]
have "\<dots> \<approx> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. replicate n (v 0) \<frown> v \<approx> v
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
replicate n (v 0) \<frown> v \<approx> v

goal (1 subgoal):
 1. replicate n (v 0) \<frown> v \<approx> v
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
replicate n (v 0) \<frown> v \<approx> v

goal (1 subgoal):
 1. \<And>n. replicate n (v 0) \<frown> v \<approx> v \<Longrightarrow> replicate (Suc n) (v 0) \<frown> v \<approx> v
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
replicate (Suc n) (v 0) \<frown> v \<approx> v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
replicate (Suc n) (v 0) \<frown> v \<approx> v

goal (1 subgoal):
 1. replicate (Suc n) (v 0) \<frown> v \<approx> v
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
replicate (Suc n) (v 0) \<frown> v \<approx> v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma replicate_stutter': "u \<frown> replicate n (v 0) \<frown> v \<approx> u \<frown> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<frown> replicate n (v 0) \<frown> v \<approx> u \<frown> v
[PROOF STEP]
using stutter_extend_concat replicate_stutter
[PROOF STATE]
proof (prove)
using this:
?u \<approx> ?v \<Longrightarrow> ?w \<frown> ?u \<approx> ?w \<frown> ?v
replicate ?n (?v 0) \<frown> ?v \<approx> ?v

goal (1 subgoal):
 1. u \<frown> replicate n (v 0) \<frown> v \<approx> u \<frown> v
[PROOF STEP]
by this


[STATEMENT]
lemma "(do {a \<leftarrow> E; b \<leftarrow> E; w \<leftarrow> B b a; z \<leftarrow> B a b; return_pmf (w,z)}) =
       (do {a \<leftarrow> E; b \<leftarrow> E; z \<leftarrow> B a b; w \<leftarrow> B b a; return_pmf (w,z)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<bind> (\<lambda>a. E \<bind> (\<lambda>b. B b a \<bind> (\<lambda>w. B a b \<bind> (\<lambda>z. return_pmf (w, z))))) = E \<bind> (\<lambda>a. E \<bind> (\<lambda>b. B a b \<bind> (\<lambda>z. B b a \<bind> (\<lambda>w. return_pmf (w, z)))))
[PROOF STEP]
by (simp)


[STATEMENT]
lemma "do {y \<leftarrow> A; x \<leftarrow> A; z \<leftarrow> B x y y; w \<leftarrow> B x x y; Some (x,y)} =
       do {x \<leftarrow> A; y \<leftarrow> A; z \<leftarrow> B x x y; w \<leftarrow> B x y y; Some (x,y)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<bind> (\<lambda>y. A \<bind> (\<lambda>x. B x y y \<bind> (\<lambda>z. B x x y \<bind> (\<lambda>w. Some (x, y))))) = A \<bind> (\<lambda>x. A \<bind> (\<lambda>y. B x x y \<bind> (\<lambda>z. B x y y \<bind> (\<lambda>w. Some (x, y)))))
[PROOF STEP]
by (simp)


[STATEMENT]
lemma "do {y \<leftarrow> A; x \<leftarrow> A; z \<leftarrow> B x y y; w \<leftarrow> B x x y; {x,y}} =
       do {x \<leftarrow> A; y \<leftarrow> A; z \<leftarrow> B x x y; w \<leftarrow> B x y y; {x,y}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<bind> (\<lambda>y. A \<bind> (\<lambda>x. B x y y \<bind> (\<lambda>z. B x x y \<bind> (\<lambda>w. {x, y})))) = A \<bind> (\<lambda>x. A \<bind> (\<lambda>y. B x x y \<bind> (\<lambda>z. B x y y \<bind> (\<lambda>w. {x, y}))))
[PROOF STEP]
by (simp)


[STATEMENT]
lemma "do {y \<leftarrow> A; x \<leftarrow> A; z \<leftarrow> B x y y; w \<leftarrow> B x x y; return_pmf (x,y)} =
       do {x \<leftarrow> A; y \<leftarrow> A; z \<leftarrow> B x x y; w \<leftarrow> B x y y; return_pmf (x,y)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<bind> (\<lambda>y. A \<bind> (\<lambda>x. B x y y \<bind> (\<lambda>z. B x x y \<bind> (\<lambda>w. return_pmf (x, y))))) = A \<bind> (\<lambda>x. A \<bind> (\<lambda>y. B x x y \<bind> (\<lambda>z. B x y y \<bind> (\<lambda>w. return_pmf (x, y)))))
[PROOF STEP]
by (simp)


[STATEMENT]
lemma "do {x \<leftarrow> A 0; y \<leftarrow> A x; w \<leftarrow> B y y; z \<leftarrow> B x y; a \<leftarrow> C; Predicate.single (a,a)} =
       do {x \<leftarrow> A 0; y \<leftarrow> A x; z \<leftarrow> B x y; w \<leftarrow> B y y; a \<leftarrow> C; Predicate.single (a,a)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A (0::'b) \<bind> (\<lambda>x. A x \<bind> (\<lambda>y. B y y \<bind> (\<lambda>w. B x y \<bind> (\<lambda>z. C \<bind> (\<lambda>a. Predicate.single (a, a)))))) = A (0::'b) \<bind> (\<lambda>x. A x \<bind> (\<lambda>y. B x y \<bind> (\<lambda>z. B y y \<bind> (\<lambda>w. C \<bind> (\<lambda>a. Predicate.single (a, a))))))
[PROOF STEP]
by (simp)


[STATEMENT]
lemma "do {x \<leftarrow> A 0; y \<leftarrow> A x; z \<leftarrow> B x y; w \<leftarrow> B y y; a \<leftarrow> C; return_pmf (a,a)} =
       do {x \<leftarrow> A 0; y \<leftarrow> A x; z \<leftarrow> B y y; w \<leftarrow> B x y; a \<leftarrow> C; return_pmf (a,a)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A (0::'b) \<bind> (\<lambda>x. A x \<bind> (\<lambda>y. B x y \<bind> (\<lambda>z. B y y \<bind> (\<lambda>w. C \<bind> (\<lambda>a. return_pmf (a, a)))))) = A (0::'b) \<bind> (\<lambda>x. A x \<bind> (\<lambda>y. B y y \<bind> (\<lambda>z. B x y \<bind> (\<lambda>w. C \<bind> (\<lambda>a. return_pmf (a, a))))))
[PROOF STEP]
by (simp)


[STATEMENT]
lemma "do {x \<leftarrow> B; z \<leftarrow> C x; d \<leftarrow> E z x; a \<leftarrow> D z x; y \<leftarrow> A; return_pmf (x,y)} =
       do {y \<leftarrow> A; x \<leftarrow> B; z \<leftarrow> C x; a \<leftarrow> D z x; d \<leftarrow> E z x; return_pmf (x,y)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<bind> (\<lambda>x. C x \<bind> (\<lambda>z. E z x \<bind> (\<lambda>d. D z x \<bind> (\<lambda>a. A \<bind> (\<lambda>y. return_pmf (x, y)))))) = A \<bind> (\<lambda>y. B \<bind> (\<lambda>x. C x \<bind> (\<lambda>z. D z x \<bind> (\<lambda>a. E z x \<bind> (\<lambda>d. return_pmf (x, y))))))
[PROOF STEP]
by (simp)


[STATEMENT]
lemma
  "do {
      x \<leftarrow> sample_uniform (order \<G>);
      y \<leftarrow> sample_uniform (order \<G>);
      z \<leftarrow> sample_uniform (order \<G>);
      b \<leftarrow> coin_spmf;
      ((msg1, msg2), \<sigma>) \<leftarrow> \1 (f x);
      _ :: unit \<leftarrow> assert_spmf (valid_plain msg1 \<and> valid_plain msg2);
      guess \<leftarrow> \2 (f y, xor (f z) (if b then msg1 else msg2)) \<sigma>;
      return_spmf (guess \<longleftrightarrow> b)
    } = do {
      x \<leftarrow> sample_uniform (order \<G>);
      y \<leftarrow> sample_uniform (order \<G>);
      ((msg1, msg2), \<sigma>) \<leftarrow> \1 (f x);
      _ :: unit \<leftarrow> assert_spmf (valid_plain msg1 \<and> valid_plain msg2);
      b \<leftarrow> coin_spmf;
      x \<leftarrow> sample_uniform (order \<G>);
      guess \<leftarrow> \2 (f y, xor (f x) (if b then msg1 else msg2)) \<sigma>;
      return_spmf (guess \<longleftrightarrow> b)
    }" for xor
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. sample_uniform (order \<G>) \<bind> (\<lambda>z. coin_spmf \<bind> (\<lambda>b. \1 (f x) \<bind> (\<lambda>((msg1, msg2), \<sigma>). assert_spmf (valid_plain msg1 \<and> valid_plain msg2) \<bind> (\<lambda>_. \2 (f y, xor (f z) (if b then msg1 else msg2)) \<sigma> \<bind> (\<lambda>guess. return_spmf (guess = b)))))))) = sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. \1 (f x) \<bind> (\<lambda>((msg1, msg2), \<sigma>). assert_spmf (valid_plain msg1 \<and> valid_plain msg2) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>b. sample_uniform (order \<G>) \<bind> (\<lambda>x. \2 (f y, xor (f x) (if b then msg1 else msg2)) \<sigma> \<bind> (\<lambda>guess. return_spmf (guess = b))))))))
[PROOF STEP]
by (simp add: split_def)


[STATEMENT]
lemma elgamal_step3:
  "do {
      x \<leftarrow> sample_uniform (order \<G>);
      y \<leftarrow> sample_uniform (order \<G>);
      b \<leftarrow> coin_spmf;
      p \<leftarrow> \1 (f x);
      _ \<leftarrow> assert_spmf (valid_plain (fst (fst p)) \<and> valid_plain (snd (fst p)));
      guess \<leftarrow>
        \2 (f y, xor (f (x * y)) (if b then fst (fst p) else snd (fst p)))
         (snd p);
      return_spmf (guess \<longleftrightarrow> b)
    }  = do {
      y \<leftarrow> sample_uniform (order \<G>);
      b \<leftarrow> coin_spmf;
      p \<leftarrow> \1 (f y);
      _ \<leftarrow> assert_spmf (valid_plain (fst (fst p)) \<and> valid_plain (snd (fst p)));
      ya \<leftarrow> sample_uniform (order \<G>);
      b' \<leftarrow> \2 (f ya,
                 xor (f (y * ya)) (if b then fst (fst p) else snd (fst p)))
             (snd p);
      return_spmf (b' \<longleftrightarrow> b)
    }" for xor
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform (order \<G>) \<bind> (\<lambda>x. sample_uniform (order \<G>) \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>b. \1 (f x) \<bind> (\<lambda>p. assert_spmf (valid_plain (fst (fst p)) \<and> valid_plain (snd (fst p))) \<bind> (\<lambda>_. \2 (f y, xor (f (x * y)) (if b then fst (fst p) else snd (fst p))) (snd p) \<bind> (\<lambda>guess. return_spmf (guess = b))))))) = sample_uniform (order \<G>) \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>b. \1 (f y) \<bind> (\<lambda>p. assert_spmf (valid_plain (fst (fst p)) \<and> valid_plain (snd (fst p))) \<bind> (\<lambda>_. sample_uniform (order \<G>) \<bind> (\<lambda>ya. \2 (f ya, xor (f (y * ya)) (if b then fst (fst p) else snd (fst p))) (snd p) \<bind> (\<lambda>b'. return_spmf (b' = b)))))))
[PROOF STEP]
by (simp)


[STATEMENT]
lemma "do {a \<leftarrow> A; b \<leftarrow> A; Some (a \<and> b, b)} =
       do {a \<leftarrow> A; b \<leftarrow> A; Some (a \<and> b, a)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<bind> (\<lambda>a. A \<bind> (\<lambda>b. Some (a \<and> b, b))) = A \<bind> (\<lambda>a. A \<bind> (\<lambda>b. Some (a \<and> b, a)))
[PROOF STEP]
apply (simp add: conj_comms)?       \<comment> \<open>no progress made\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<bind> (\<lambda>a. A \<bind> (\<lambda>b. Some (a \<and> b, b))) = A \<bind> (\<lambda>a. A \<bind> (\<lambda>b. Some (a \<and> b, a)))
[PROOF STEP]
apply (rewrite option_bind_commute) \<comment> \<open>force a particular binder order\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<bind> (\<lambda>y. A \<bind> (\<lambda>a. Some (a \<and> y, y))) = A \<bind> (\<lambda>a. A \<bind> (\<lambda>b. Some (a \<and> b, a)))
[PROOF STEP]
apply (simp only: conj_comms)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma vebt_buildupi_rule_basic[sep_heap_rules]: "n > 0 \<Longrightarrow> <emp> vebt_buildupi n <\<lambda> r. vebt_assn n {} r >"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> <emp> vebt_buildupi n <vebt_assn n {}>
[PROOF STEP]
unfolding vebt_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> <emp> vebt_buildupi n <\<lambda>r. \<exists>\<^sub>At. vebt_assn_raw t r * \<up> ({} = set_vebt t \<and> invar_vebt t n)>
[PROOF STEP]
apply(rule  post_exI_rule[where x = "vebt_buildup n"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> <emp> vebt_buildupi n <\<lambda>r. vebt_assn_raw (vebt_buildup n) r * \<up> ({} = set_vebt (vebt_buildup n) \<and> invar_vebt (vebt_buildup n) n)>
[PROOF STEP]
using builupicorr[of n] invar_vebt_buildup[of n] set_vebt_buildup[of n]
[PROOF STATE]
proof (prove)
using this:
<emp> vebt_buildupi n <vebt_assn_raw (vebt_buildup n)>
invar_vebt (vebt_buildup n) n = (0 < n)
set_vebt (vebt_buildup n) = {}

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> <emp> vebt_buildupi n <\<lambda>r. vebt_assn_raw (vebt_buildup n) r * \<up> ({} = set_vebt (vebt_buildup n) \<and> invar_vebt (vebt_buildup n) n)>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma vebt_buildupi_rule: "<\<up> (n > 0)> vebt_buildupi  n <\<lambda> r. vebt_assn n {} r > T[10 * 2^n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<up> (0 < n)> vebt_buildupi n <vebt_assn n {}> T[10 * 2 ^ n]
[PROOF STEP]
unfolding vebt_assn_def htt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<up> (0 < n)> vebt_buildupi n <\<lambda>r. \<exists>\<^sub>At. vebt_assn_raw t r * \<up> ({} = set_vebt t \<and> invar_vebt t n)> \<and> (\<forall>h as. (h, as) \<Turnstile> \<up> (0 < n) \<longrightarrow> time (vebt_buildupi n) h \<le> 10 * 2 ^ n)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. <\<up> (0 < n)> vebt_buildupi n <\<lambda>r. \<exists>\<^sub>At. vebt_assn_raw t r * \<up> ({} = set_vebt t \<and> invar_vebt t n)>
 2. \<forall>h as. (h, as) \<Turnstile> \<up> (0 < n) \<longrightarrow> time (vebt_buildupi n) h \<le> 10 * 2 ^ n
[PROOF STEP]
apply(rule  post_exI_rule[where x = "vebt_buildup n"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. <\<up> (0 < n)> vebt_buildupi n <\<lambda>r. vebt_assn_raw (vebt_buildup n) r * \<up> ({} = set_vebt (vebt_buildup n) \<and> invar_vebt (vebt_buildup n) n)>
 2. \<forall>h as. (h, as) \<Turnstile> \<up> (0 < n) \<longrightarrow> time (vebt_buildupi n) h \<le> 10 * 2 ^ n
[PROOF STEP]
using vebt_buildupi_rule[of n] invar_vebt_buildup[of  n] set_vebt_buildup[of n]
[PROOF STATE]
proof (prove)
using this:
<\<up> (0 < n)> vebt_buildupi n <vebt_assn_raw (vebt_buildup n)> T[10 * 2 ^ n]
invar_vebt (vebt_buildup n) n = (0 < n)
set_vebt (vebt_buildup n) = {}

goal (2 subgoals):
 1. <\<up> (0 < n)> vebt_buildupi n <\<lambda>r. vebt_assn_raw (vebt_buildup n) r * \<up> ({} = set_vebt (vebt_buildup n) \<and> invar_vebt (vebt_buildup n) n)>
 2. \<forall>h as. (h, as) \<Turnstile> \<up> (0 < n) \<longrightarrow> time (vebt_buildupi n) h \<le> 10 * 2 ^ n
[PROOF STEP]
unfolding htt_def
[PROOF STATE]
proof (prove)
using this:
<\<up> (0 < n)> vebt_buildupi n <vebt_assn_raw (vebt_buildup n)> \<and> (\<forall>h as. (h, as) \<Turnstile> \<up> (0 < n) \<longrightarrow> time (vebt_buildupi n) h \<le> 10 * 2 ^ n)
invar_vebt (vebt_buildup n) n = (0 < n)
set_vebt (vebt_buildup n) = {}

goal (2 subgoals):
 1. <\<up> (0 < n)> vebt_buildupi n <\<lambda>r. vebt_assn_raw (vebt_buildup n) r * \<up> ({} = set_vebt (vebt_buildup n) \<and> invar_vebt (vebt_buildup n) n)>
 2. \<forall>h as. (h, as) \<Turnstile> \<up> (0 < n) \<longrightarrow> time (vebt_buildupi n) h \<le> 10 * 2 ^ n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h as. (h, as) \<Turnstile> \<up> (0 < n) \<longrightarrow> time (vebt_buildupi n) h \<le> 10 * 2 ^ n
[PROOF STEP]
using TBOUND_buildupi[of n]
[PROOF STATE]
proof (prove)
using this:
0 < n \<Longrightarrow> TBOUND (vebt_buildupi n) (10 * 2 ^ n)

goal (1 subgoal):
 1. \<forall>h as. (h, as) \<Turnstile> \<up> (0 < n) \<longrightarrow> time (vebt_buildupi n) h \<le> 10 * 2 ^ n
[PROOF STEP]
unfolding TBOUND_def
[PROOF STATE]
proof (prove)
using this:
0 < n \<Longrightarrow> \<forall>h. time (vebt_buildupi n) h \<le> 10 * 2 ^ n

goal (1 subgoal):
 1. \<forall>h as. (h, as) \<Turnstile> \<up> (0 < n) \<longrightarrow> time (vebt_buildupi n) h \<le> 10 * 2 ^ n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma vebt_memberi_rule: "<vebt_assn n s ti> vebt_memberi ti x <\<lambda> r. vebt_assn n s ti *  \<up>(r = (x \<in> s))>T[5 + 5 * (nat \<lceil>lb n \<rceil>)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <vebt_assn n s ti> vebt_memberi ti x <\<lambda>r. vebt_assn n s ti * \<up> (r = (x \<in> s))> T[5 + 5 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
unfolding vebt_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)> vebt_memberi ti x <\<lambda>r. (\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)) * \<up> (r = (x \<in> s))> T[5 + 5 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(rule norm_pre_ex_rule_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. <vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)> vebt_memberi ti x <\<lambda>r. (\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)) * \<up> (r = (x \<in> s))> T[5 + 5 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(clarsimp simp: norm_pre_pure_iff_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> <vebt_assn_raw t ti> vebt_memberi ti x <\<lambda>r. \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> (r = (x \<in> set_vebt t))> T[5 + 5 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(rule htt_cons_rule[OF htt_vebt_memberi_invar_vebt])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> invar_vebt (?t6 t) (?n6 t)
 2. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti \<Longrightarrow>\<^sub>A vebt_assn_raw (?t6 t) ti
 3. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw (?t6 t) ti * \<up> (r = vebt_member (?t6 t) x) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> (r = (x \<in> set_vebt t))
 4. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 5 + 5 * nat \<lceil>log 2 (real (?n6 t))\<rceil> \<le> 5 + 5 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti \<Longrightarrow>\<^sub>A vebt_assn_raw t ti
 2. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti * \<up> (r = vebt_member t x) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> (r = (x \<in> set_vebt t))
 3. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 5 + 5 * nat \<lceil>log 2 (real n)\<rceil> \<le> 5 + 5 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti * \<up> (r = vebt_member t x) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> (r = (x \<in> set_vebt t))
 2. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 5 + 5 * nat \<lceil>log 2 (real n)\<rceil> \<le> 5 + 5 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply (sep_auto simp: member_correct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 5 + 5 * nat \<lceil>log 2 (real n)\<rceil> \<le> 5 + 5 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done