[STATEMENT]
lemma ufa_compress_aux:
  assumes I: "ufa_invar l"
  assumes L[simp]: "x<length l"
  shows "ufa_invar (l[x := rep_of l x])"
  and "\<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ufa_invar (l[x := rep_of l x]) &&& \<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ufa_invar (l[x := rep_of l x])
 2. \<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ufa_invar (l[x := rep_of l x])
 2. \<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ufa_invar (l[x := rep_of l x])
 2. \<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
assume "i<length (l[x := rep_of l x])"
[PROOF STATE]
proof (state)
this:
i < length (l[x := rep_of l x])

goal (2 subgoals):
 1. ufa_invar (l[x := rep_of l x])
 2. \<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
hence IL: "i<length l"
[PROOF STATE]
proof (prove)
using this:
i < length (l[x := rep_of l x])

goal (1 subgoal):
 1. i < length l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < length l

goal (2 subgoals):
 1. ufa_invar (l[x := rep_of l x])
 2. \<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
have G1: "l[x := rep_of l x] ! i < length (l[x := rep_of l x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l[x := rep_of l x] ! i < length (l[x := rep_of l x])
[PROOF STEP]
using I IL
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
i < length l

goal (1 subgoal):
 1. l[x := rep_of l x] ! i < length (l[x := rep_of l x])
[PROOF STEP]
by (auto dest: ufa_invarD[OF I] simp: nth_list_update rep_of_bound)
[PROOF STATE]
proof (state)
this:
l[x := rep_of l x] ! i < length (l[x := rep_of l x])

goal (2 subgoals):
 1. ufa_invar (l[x := rep_of l x])
 2. \<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
from I IL
[PROOF STATE]
proof (chain)
picking this:
ufa_invar l
i < length l
[PROOF STEP]
have G2: "rep_of (l[x := rep_of l x]) i = rep_of l i
      \<and> rep_of_dom (l[x := rep_of l x], i)"
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
i < length l

goal (1 subgoal):
 1. rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)
[PROOF STEP]
proof (induct rule: rep_of_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i = i\<rbrakk> \<Longrightarrow> rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)
 2. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i)\<rbrakk> \<Longrightarrow> rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)
[PROOF STEP]
case (base i)
[PROOF STATE]
proof (state)
this:
ufa_invar l
i < length l
l ! i = i

goal (2 subgoals):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i = i\<rbrakk> \<Longrightarrow> rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)
 2. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i)\<rbrakk> \<Longrightarrow> rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
i < length l
l ! i = i

goal (1 subgoal):
 1. rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)
[PROOF STEP]
apply (cases "x=i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ufa_invar l; i < length l; l ! i = i; x = i\<rbrakk> \<Longrightarrow> rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)
 2. \<lbrakk>ufa_invar l; i < length l; l ! i = i; x \<noteq> i\<rbrakk> \<Longrightarrow> rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)
[PROOF STEP]
apply (auto intro: rep_of.domintros simp: rep_of_refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i)\<rbrakk> \<Longrightarrow> rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i)\<rbrakk> \<Longrightarrow> rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)
[PROOF STEP]
case (step i)
[PROOF STATE]
proof (state)
this:
ufa_invar l
i < length l
l ! i \<noteq> i
rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i)

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i)\<rbrakk> \<Longrightarrow> rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)
[PROOF STEP]
hence D: "rep_of_dom (l[x := rep_of l x], i)"
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
i < length l
l ! i \<noteq> i
rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i)

goal (1 subgoal):
 1. rep_of_dom (l[x := rep_of l x], i)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i)\<rbrakk> \<Longrightarrow> rep_of_dom (l[x := rep_of l x], i)
[PROOF STEP]
apply (rule rep_of.domintros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i); l[x := rep_of l x] ! i \<noteq> i\<rbrakk> \<Longrightarrow> rep_of_dom (l[x := rep_of l x], l[x := rep_of l x] ! i)
[PROOF STEP]
apply (cases "x=i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i); l[x := rep_of l x] ! i \<noteq> i; x = i\<rbrakk> \<Longrightarrow> rep_of_dom (l[x := rep_of l x], l[x := rep_of l x] ! i)
 2. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i); l[x := rep_of l x] ! i \<noteq> i; x \<noteq> i\<rbrakk> \<Longrightarrow> rep_of_dom (l[x := rep_of l x], l[x := rep_of l x] ! i)
[PROOF STEP]
apply (auto intro: rep_of.domintros simp: rep_of_min)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rep_of_dom (l[x := rep_of l x], i)

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i)\<rbrakk> \<Longrightarrow> rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
rep_of_dom (l[x := rep_of l x], i)

goal (1 subgoal):
 1. rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep_of_dom (l[x := rep_of l x], i) \<Longrightarrow> rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
i < length l
l ! i \<noteq> i
rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i)

goal (1 subgoal):
 1. rep_of_dom (l[x := rep_of l x], i) \<Longrightarrow> rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rep_of_dom (l[x := rep_of l x], i); ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i)\<rbrakk> \<Longrightarrow> rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
apply (subst rep_of.psimps[OF D])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rep_of_dom (l[x := rep_of l x], i); ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i)\<rbrakk> \<Longrightarrow> (if l[x := rep_of l x] ! i = i then i else rep_of (l[x := rep_of l x]) (l[x := rep_of l x] ! i)) = rep_of l i
[PROOF STEP]
apply (cases "x=i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rep_of_dom (l[x := rep_of l x], i); ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i); x = i\<rbrakk> \<Longrightarrow> (if l[x := rep_of l x] ! i = i then i else rep_of (l[x := rep_of l x]) (l[x := rep_of l x] ! i)) = rep_of l i
 2. \<lbrakk>rep_of_dom (l[x := rep_of l x], i); ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (l[x := rep_of l x]) (l ! i) = rep_of l (l ! i) \<and> rep_of_dom (l[x := rep_of l x], l ! i); x \<noteq> i\<rbrakk> \<Longrightarrow> (if l[x := rep_of l x] ! i = i then i else rep_of (l[x := rep_of l x]) (l[x := rep_of l x] ! i)) = rep_of l i
[PROOF STEP]
apply (auto simp: rep_of_min rep_of_idx)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rep_of_dom (l[i := rep_of l i], i); ufa_invar l; i < length l; l ! i \<noteq> i; x = i; rep_of (l[i := rep_of l i]) (l ! i) = rep_of l i; rep_of_dom (l[i := rep_of l i], l ! i); rep_of l i \<noteq> i\<rbrakk> \<Longrightarrow> rep_of (l[i := rep_of l i]) (rep_of l i) = rep_of l i
[PROOF STEP]
apply (subst rep_of.psimps[where i="rep_of l i"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rep_of_dom (l[i := rep_of l i], i); ufa_invar l; i < length l; l ! i \<noteq> i; x = i; rep_of (l[i := rep_of l i]) (l ! i) = rep_of l i; rep_of_dom (l[i := rep_of l i], l ! i); rep_of l i \<noteq> i\<rbrakk> \<Longrightarrow> rep_of_dom (l[i := rep_of l i], rep_of l i)
 2. \<lbrakk>rep_of_dom (l[i := rep_of l i], i); ufa_invar l; i < length l; l ! i \<noteq> i; x = i; rep_of (l[i := rep_of l i]) (l ! i) = rep_of l i; rep_of_dom (l[i := rep_of l i], l ! i); rep_of l i \<noteq> i\<rbrakk> \<Longrightarrow> (if l[i := rep_of l i] ! rep_of l i = rep_of l i then rep_of l i else rep_of (l[i := rep_of l i]) (l[i := rep_of l i] ! rep_of l i)) = rep_of l i
[PROOF STEP]
apply (auto intro: rep_of.domintros simp: rep_of_min)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)

goal (2 subgoals):
 1. ufa_invar (l[x := rep_of l x])
 2. \<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
note G1 G2
[PROOF STATE]
proof (state)
this:
l[x := rep_of l x] ! i < length (l[x := rep_of l x])
rep_of (l[x := rep_of l x]) i = rep_of l i \<and> rep_of_dom (l[x := rep_of l x], i)

goal (2 subgoals):
 1. ufa_invar (l[x := rep_of l x])
 2. \<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i2 < length (l[x := rep_of l x]) \<Longrightarrow> l[x := rep_of l x] ! ?i2 < length (l[x := rep_of l x])
?i2 < length (l[x := rep_of l x]) \<Longrightarrow> rep_of (l[x := rep_of l x]) ?i2 = rep_of l ?i2 \<and> rep_of_dom (l[x := rep_of l x], ?i2)

goal (2 subgoals):
 1. ufa_invar (l[x := rep_of l x])
 2. \<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
note G=this
[PROOF STATE]
proof (state)
this:
?i2 < length (l[x := rep_of l x]) \<Longrightarrow> l[x := rep_of l x] ! ?i2 < length (l[x := rep_of l x])
?i2 < length (l[x := rep_of l x]) \<Longrightarrow> rep_of (l[x := rep_of l x]) ?i2 = rep_of l ?i2 \<and> rep_of_dom (l[x := rep_of l x], ?i2)

goal (2 subgoals):
 1. ufa_invar (l[x := rep_of l x])
 2. \<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
thus "\<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i"
[PROOF STATE]
proof (prove)
using this:
?i2 < length (l[x := rep_of l x]) \<Longrightarrow> l[x := rep_of l x] ! ?i2 < length (l[x := rep_of l x])
?i2 < length (l[x := rep_of l x]) \<Longrightarrow> rep_of (l[x := rep_of l x]) ?i2 = rep_of l ?i2 \<and> rep_of_dom (l[x := rep_of l x], ?i2)

goal (1 subgoal):
 1. \<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i

goal (1 subgoal):
 1. ufa_invar (l[x := rep_of l x])
[PROOF STEP]
from G
[PROOF STATE]
proof (chain)
picking this:
?i2 < length (l[x := rep_of l x]) \<Longrightarrow> l[x := rep_of l x] ! ?i2 < length (l[x := rep_of l x])
?i2 < length (l[x := rep_of l x]) \<Longrightarrow> rep_of (l[x := rep_of l x]) ?i2 = rep_of l ?i2 \<and> rep_of_dom (l[x := rep_of l x], ?i2)
[PROOF STEP]
show "ufa_invar (l[x := rep_of l x])"
[PROOF STATE]
proof (prove)
using this:
?i2 < length (l[x := rep_of l x]) \<Longrightarrow> l[x := rep_of l x] ! ?i2 < length (l[x := rep_of l x])
?i2 < length (l[x := rep_of l x]) \<Longrightarrow> rep_of (l[x := rep_of l x]) ?i2 = rep_of l ?i2 \<and> rep_of_dom (l[x := rep_of l x], ?i2)

goal (1 subgoal):
 1. ufa_invar (l[x := rep_of l x])
[PROOF STEP]
by (auto simp: ufa_invar_def)
[PROOF STATE]
proof (state)
this:
ufa_invar (l[x := rep_of l x])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ufa_compress_invar:
  assumes I: "ufa_invar l"
  assumes L[simp]: "x<length l"
  shows "ufa_invar (l[x := rep_of l x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ufa_invar (l[x := rep_of l x])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
x < length l

goal (1 subgoal):
 1. ufa_invar (l[x := rep_of l x])
[PROOF STEP]
by (rule ufa_compress_aux)


[STATEMENT]
lemma ufa_compress_correct:
  assumes I: "ufa_invar l"
  assumes L[simp]: "x<length l"
  shows "ufa_\<alpha> (l[x := rep_of l x]) = ufa_\<alpha> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ufa_\<alpha> (l[x := rep_of l x]) = ufa_\<alpha> l
[PROOF STEP]
by (auto simp: ufa_\<alpha>_def ufa_compress_aux[OF I])


[STATEMENT]
lemma uf_init_rule[sep_heap_rules]:
  "<emp> uf_init n <is_uf {(i,i) |i. i<n}>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <emp> uf_init n <is_uf {(i, i) |i. i < n}>
[PROOF STEP]
unfolding uf_init_def is_uf_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <emp> Array.of_list [0..<n] \<bind> (\<lambda>l. Array.new n 1 \<bind> (\<lambda>szl. return (szl, l))) <\<lambda>(s, p). \<exists>\<^sub>Al szl. p \<mapsto>\<^sub>a l * s \<mapsto>\<^sub>a szl * \<up> (ufa_invar l \<and> ufa_\<alpha> l = {(i, i) |i. i < n} \<and> length szl = length l)>
[PROOF STEP]
by (sep_auto simp: ufa_init_correct ufa_init_invar)


[STATEMENT]
lemma uf_rep_of_rule[sep_heap_rules]: "\<lbrakk>ufa_invar l; i<length l\<rbrakk> \<Longrightarrow>
  <p\<mapsto>\<^sub>al> uf_rep_of p i <\<lambda>r. p\<mapsto>\<^sub>al * \<up>(r=rep_of l i)>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_rep_of p i <\<lambda>r. p \<mapsto>\<^sub>a l * \<up> (r = rep_of l i)>
[PROOF STEP]
apply (induct rule: rep_of_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i = i\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_rep_of p i <\<lambda>r. p \<mapsto>\<^sub>a l * \<up> (r = rep_of l i)>
 2. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; <p \<mapsto>\<^sub>a l> uf_rep_of p (l ! i) <\<lambda>r. p \<mapsto>\<^sub>a l * \<up> (r = rep_of l (l ! i))>\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_rep_of p i <\<lambda>r. p \<mapsto>\<^sub>a l * \<up> (r = rep_of l i)>
[PROOF STEP]
apply (subst uf_rep_of.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i = i\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> Array.nth p i \<bind> (\<lambda>n. if n = i then return i else uf_rep_of p n) <\<lambda>r. p \<mapsto>\<^sub>a l * \<up> (r = rep_of l i)>
 2. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; <p \<mapsto>\<^sub>a l> uf_rep_of p (l ! i) <\<lambda>r. p \<mapsto>\<^sub>a l * \<up> (r = rep_of l (l ! i))>\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_rep_of p i <\<lambda>r. p \<mapsto>\<^sub>a l * \<up> (r = rep_of l i)>
[PROOF STEP]
apply (sep_auto simp: rep_of_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; <p \<mapsto>\<^sub>a l> uf_rep_of p (l ! i) <\<lambda>r. p \<mapsto>\<^sub>a l * \<up> (r = rep_of l (l ! i))>\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_rep_of p i <\<lambda>r. p \<mapsto>\<^sub>a l * \<up> (r = rep_of l i)>
[PROOF STEP]
apply (subst uf_rep_of.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; <p \<mapsto>\<^sub>a l> uf_rep_of p (l ! i) <\<lambda>r. p \<mapsto>\<^sub>a l * \<up> (r = rep_of l (l ! i))>\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> Array.nth p i \<bind> (\<lambda>n. if n = i then return i else uf_rep_of p n) <\<lambda>r. p \<mapsto>\<^sub>a l * \<up> (r = rep_of l i)>
[PROOF STEP]
apply (sep_auto simp: rep_of_step)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma uf_compress_rule: "\<lbrakk> ufa_invar l; i<length l; ci=rep_of l i \<rbrakk> \<Longrightarrow>
  <p\<mapsto>\<^sub>al> uf_compress i ci p
  <\<lambda>_. \<exists>\<^sub>Al'. p\<mapsto>\<^sub>al' * \<up>(ufa_invar l' \<and> length l' = length l
     \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l; ci = rep_of l i\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress i ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
proof (induction rule: rep_of_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i = i; ci = rep_of l i\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress i ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
 2. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; ci = rep_of l (l ! i) \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress (l ! i) ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>; ci = rep_of l i\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress i ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
case (base i)
[PROOF STATE]
proof (state)
this:
ufa_invar l
i < length l
l ! i = i
ci = rep_of l i

goal (2 subgoals):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i = i; ci = rep_of l i\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress i ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
 2. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; ci = rep_of l (l ! i) \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress (l ! i) ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>; ci = rep_of l i\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress i ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
i < length l
l ! i = i
ci = rep_of l i

goal (1 subgoal):
 1. <p \<mapsto>\<^sub>a l> uf_compress i ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
apply (subst uf_compress.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l; l ! i = i; ci = rep_of l i\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> if i = ci then return () else Array.nth p i \<bind> (\<lambda>ni. uf_compress ni ci p \<bind> (\<lambda>_. Array.upd i ci p \<bind> (\<lambda>_. return ()))) <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
apply (sep_auto simp: rep_of_refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
<p \<mapsto>\<^sub>a l> uf_compress i ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; ci = rep_of l (l ! i) \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress (l ! i) ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>; ci = rep_of l i\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress i ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; ci = rep_of l (l ! i) \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress (l ! i) ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>; ci = rep_of l i\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress i ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
case (step i)
[PROOF STATE]
proof (state)
this:
ufa_invar l
i < length l
l ! i \<noteq> i
ci = rep_of l (l ! i) \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress (l ! i) ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
ci = rep_of l i

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; ci = rep_of l (l ! i) \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress (l ! i) ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>; ci = rep_of l i\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress i ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
note SS = \<open>ufa_invar l\<close> \<open>i<length l\<close> \<open>l!i\<noteq>i\<close> \<open>ci = rep_of l i\<close>
[PROOF STATE]
proof (state)
this:
ufa_invar l
i < length l
l ! i \<noteq> i
ci = rep_of l i

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; ci = rep_of l (l ! i) \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress (l ! i) ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>; ci = rep_of l i\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress i ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
from step.IH
[PROOF STATE]
proof (chain)
picking this:
ci = rep_of l (l ! i) \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress (l ! i) ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
have IH':
    "<p \<mapsto>\<^sub>a l>
       uf_compress (l ! i) (rep_of l i) p
     <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' *
        \<up> (ufa_invar l' \<and> length l = length l'
           \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i))
     >"
[PROOF STATE]
proof (prove)
using this:
ci = rep_of l (l ! i) \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress (l ! i) ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>

goal (1 subgoal):
 1. <p \<mapsto>\<^sub>a l> uf_compress (l ! i) (rep_of l i) p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i))>
[PROOF STEP]
apply (simp add: rep_of_idx SS)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <p \<mapsto>\<^sub>a l> uf_compress (l ! i) (rep_of l i) p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress (l ! i) (rep_of l i) p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i))>
[PROOF STEP]
apply (erule
      back_subst[OF _ cong[OF cong[OF arg_cong[where f=hoare_triple]]]])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. p \<mapsto>\<^sub>a l = p \<mapsto>\<^sub>a l
 2. uf_compress (l ! i) (rep_of l i) p = uf_compress (l ! i) (rep_of l i) p
 3. (\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))) = (\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i)))
[PROOF STEP]
apply (auto) [2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))) = (\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i)))
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>_. (\<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))) = (\<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i)))
[PROOF STEP]
apply (rule ent_iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i)) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i))
 2. \<And>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i)) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))
[PROOF STEP]
apply sep_auto+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
<p \<mapsto>\<^sub>a l> uf_compress (l ! i) (rep_of l i) p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i))>

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; ci = rep_of l (l ! i) \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress (l ! i) ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>; ci = rep_of l i\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress i ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <p \<mapsto>\<^sub>a l> uf_compress i ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
apply (subst uf_compress.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <p \<mapsto>\<^sub>a l> if i = ci then return () else Array.nth p i \<bind> (\<lambda>ni. uf_compress ni ci p \<bind> (\<lambda>_. Array.upd i ci p \<bind> (\<lambda>_. return ()))) <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
apply (sep_auto simp: SS)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i \<noteq> rep_of l i \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_compress (l ! i) (rep_of l i) p <?R30>
 2. \<And>x. i \<noteq> rep_of l i \<Longrightarrow> <?R30 x> Array.upd i (rep_of l i) p \<bind> (\<lambda>_. return ()) <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
apply (rule IH')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. i \<noteq> rep_of l i \<Longrightarrow> <\<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i))> Array.upd i (rep_of l i) p \<bind> (\<lambda>_. return ()) <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
using SS
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
i < length l
l ! i \<noteq> i
ci = rep_of l i

goal (1 subgoal):
 1. \<And>x. i \<noteq> rep_of l i \<Longrightarrow> <\<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i))> Array.upd i (rep_of l i) p \<bind> (\<lambda>_. return ()) <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
apply (sep_auto (plain))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>l' x xa. \<lbrakk>i \<noteq> rep_of l' i; ufa_invar l; i < length l'; l ! i \<noteq> i; ci = rep_of l' i; ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i); x = p; \<exists>h. h \<Turnstile> p \<mapsto>\<^sub>a l'[i := rep_of l' i] * \<up> (xa = ())\<rbrakk> \<Longrightarrow> ufa_invar (l'[i := rep_of l' i])
 2. \<And>l' x xa. \<lbrakk>i \<noteq> rep_of l' i; ufa_invar l; i < length l'; l ! i \<noteq> i; ci = rep_of l' i; ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i); x = p; \<exists>h. h \<Turnstile> p \<mapsto>\<^sub>a l'[i := rep_of l' i] * \<up> (xa = ())\<rbrakk> \<Longrightarrow> length (l'[i := rep_of l' i]) = length l'
 3. \<And>l' x xa. \<lbrakk>i \<noteq> rep_of l' i; ufa_invar l; i < length l'; l ! i \<noteq> i; ci = rep_of l' i; ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i); x = p; \<exists>h. h \<Turnstile> p \<mapsto>\<^sub>a l'[i := rep_of l' i] * \<up> (xa = ())\<rbrakk> \<Longrightarrow> \<forall>i<length l'. rep_of (l'[i := rep_of l' i]) i = rep_of l' i
[PROOF STEP]
using ufa_compress_invar
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ufa_invar ?l; ?x < length ?l\<rbrakk> \<Longrightarrow> ufa_invar (?l[?x := rep_of ?l ?x])

goal (3 subgoals):
 1. \<And>l' x xa. \<lbrakk>i \<noteq> rep_of l' i; ufa_invar l; i < length l'; l ! i \<noteq> i; ci = rep_of l' i; ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i); x = p; \<exists>h. h \<Turnstile> p \<mapsto>\<^sub>a l'[i := rep_of l' i] * \<up> (xa = ())\<rbrakk> \<Longrightarrow> ufa_invar (l'[i := rep_of l' i])
 2. \<And>l' x xa. \<lbrakk>i \<noteq> rep_of l' i; ufa_invar l; i < length l'; l ! i \<noteq> i; ci = rep_of l' i; ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i); x = p; \<exists>h. h \<Turnstile> p \<mapsto>\<^sub>a l'[i := rep_of l' i] * \<up> (xa = ())\<rbrakk> \<Longrightarrow> length (l'[i := rep_of l' i]) = length l'
 3. \<And>l' x xa. \<lbrakk>i \<noteq> rep_of l' i; ufa_invar l; i < length l'; l ! i \<noteq> i; ci = rep_of l' i; ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i); x = p; \<exists>h. h \<Turnstile> p \<mapsto>\<^sub>a l'[i := rep_of l' i] * \<up> (xa = ())\<rbrakk> \<Longrightarrow> \<forall>i<length l'. rep_of (l'[i := rep_of l' i]) i = rep_of l' i
[PROOF STEP]
apply fastforce []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l' x xa. \<lbrakk>i \<noteq> rep_of l' i; ufa_invar l; i < length l'; l ! i \<noteq> i; ci = rep_of l' i; ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i); x = p; \<exists>h. h \<Turnstile> p \<mapsto>\<^sub>a l'[i := rep_of l' i] * \<up> (xa = ())\<rbrakk> \<Longrightarrow> length (l'[i := rep_of l' i]) = length l'
 2. \<And>l' x xa. \<lbrakk>i \<noteq> rep_of l' i; ufa_invar l; i < length l'; l ! i \<noteq> i; ci = rep_of l' i; ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i); x = p; \<exists>h. h \<Turnstile> p \<mapsto>\<^sub>a l'[i := rep_of l' i] * \<up> (xa = ())\<rbrakk> \<Longrightarrow> \<forall>i<length l'. rep_of (l'[i := rep_of l' i]) i = rep_of l' i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l' x xa. \<lbrakk>i \<noteq> rep_of l' i; ufa_invar l; i < length l'; l ! i \<noteq> i; ci = rep_of l' i; ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i); x = p; \<exists>h. h \<Turnstile> p \<mapsto>\<^sub>a l'[i := rep_of l' i] * \<up> (xa = ())\<rbrakk> \<Longrightarrow> \<forall>i<length l'. rep_of (l'[i := rep_of l' i]) i = rep_of l' i
[PROOF STEP]
using ufa_compress_aux(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ufa_invar ?l; ?x < length ?l\<rbrakk> \<Longrightarrow> \<forall>i<length ?l. rep_of (?l[?x := rep_of ?l ?x]) i = rep_of ?l i

goal (1 subgoal):
 1. \<And>l' x xa. \<lbrakk>i \<noteq> rep_of l' i; ufa_invar l; i < length l'; l ! i \<noteq> i; ci = rep_of l' i; ufa_invar l' \<and> length l = length l' \<and> (\<forall>i<length l'. rep_of l i = rep_of l' i); x = p; \<exists>h. h \<Turnstile> p \<mapsto>\<^sub>a l'[i := rep_of l' i] * \<up> (xa = ())\<rbrakk> \<Longrightarrow> \<forall>i<length l'. rep_of (l'[i := rep_of l' i]) i = rep_of l' i
[PROOF STEP]
apply fastforce []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
<p \<mapsto>\<^sub>a l> uf_compress i ci p <\<lambda>_. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uf_rep_of_c_rule[sep_heap_rules]: "\<lbrakk>ufa_invar l; i<length l\<rbrakk> \<Longrightarrow>
  <p\<mapsto>\<^sub>al> uf_rep_of_c p i <\<lambda>r. \<exists>\<^sub>Al'. p\<mapsto>\<^sub>al'
    * \<up>(r=rep_of l i \<and> ufa_invar l'
       \<and> length l' = length l
       \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_rep_of_c p i <\<lambda>r. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (r = rep_of l i \<and> ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
unfolding uf_rep_of_c_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> <p \<mapsto>\<^sub>a l> uf_rep_of p i \<bind> (\<lambda>ci. uf_compress i ci p \<bind> (\<lambda>_. return ci)) <\<lambda>r. \<exists>\<^sub>Al'. p \<mapsto>\<^sub>a l' * \<up> (r = rep_of l i \<and> ufa_invar l' \<and> length l' = length l \<and> (\<forall>i<length l. rep_of l' i = rep_of l i))>
[PROOF STEP]
by (sep_auto heap: uf_compress_rule)


[STATEMENT]
lemma cnv_to_ufa_\<alpha>_eq:
  "\<lbrakk>(\<forall>i<length l. rep_of l' i = rep_of l i); length l = length l'\<rbrakk>
  \<Longrightarrow> (ufa_\<alpha> l = ufa_\<alpha> l')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i<length l. rep_of l' i = rep_of l i; length l = length l'\<rbrakk> \<Longrightarrow> ufa_\<alpha> l = ufa_\<alpha> l'
[PROOF STEP]
unfolding ufa_\<alpha>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i<length l. rep_of l' i = rep_of l i; length l = length l'\<rbrakk> \<Longrightarrow> {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y} = {(x, y). x < length l' \<and> y < length l' \<and> rep_of l' x = rep_of l' y}
[PROOF STEP]
by auto


[STATEMENT]
lemma uf_cmp_rule[sep_heap_rules]:
  "<is_uf R u> uf_cmp u i j <\<lambda>r. is_uf R u * \<up>(r\<longleftrightarrow>(i,j)\<in>R)>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_uf R u> uf_cmp u i j <\<lambda>r. is_uf R u * \<up> (r = ((i, j) \<in> R))>
[PROOF STEP]
unfolding uf_cmp_def is_uf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <case u of (s, p) \<Rightarrow> \<exists>\<^sub>Al szl. p \<mapsto>\<^sub>a l * s \<mapsto>\<^sub>a szl * \<up> (ufa_invar l \<and> ufa_\<alpha> l = R \<and> length szl = length l)> let (s, p) = u in Array.len p \<bind> (\<lambda>n. if n \<le> i \<or> n \<le> j then return False else uf_rep_of_c p i \<bind> (\<lambda>ci. uf_rep_of_c p j \<bind> (\<lambda>cj. return (ci = cj)))) <\<lambda>r. (case u of (s, p) \<Rightarrow> \<exists>\<^sub>Al szl. p \<mapsto>\<^sub>a l * s \<mapsto>\<^sub>a szl * \<up> (ufa_invar l \<and> ufa_\<alpha> l = R \<and> length szl = length l)) * \<up> (r = ((i, j) \<in> R))>
[PROOF STEP]
apply (sep_auto dest: ufa_\<alpha>_lenD simp: not_le split: prod.split)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2 l szl l' l'a a b aa ba. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l; ufa_invar l'; ufa_invar l'a; length l' = length l; \<forall>i<length l. rep_of l' i = rep_of l i; length l'a = length l; \<forall>i<length l. rep_of l'a i = rep_of l i; (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl; (aa, ba) \<in> ufa_\<alpha> l'a\<rbrakk> \<Longrightarrow> (aa, ba) \<in> ufa_\<alpha> l
 2. \<And>x1 x2 l szl l' l'a a b aa ba. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l; ufa_invar l'; ufa_invar l'a; length l' = length l; \<forall>i<length l. rep_of l' i = rep_of l i; length l'a = length l; \<forall>i<length l. rep_of l'a i = rep_of l i; (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl; (aa, ba) \<in> ufa_\<alpha> l\<rbrakk> \<Longrightarrow> (aa, ba) \<in> ufa_\<alpha> l'a
 3. \<And>x1 x2 l szl l' l'a. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l; ufa_invar l'; ufa_invar l'a; length l' = length l; \<forall>i<length l. rep_of l' i = rep_of l i; length l'a = length l; \<forall>i<length l. rep_of l'a i = rep_of l i; \<exists>h. h \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl\<rbrakk> \<Longrightarrow> (rep_of l i = rep_of l j) = ((i, j) \<in> ufa_\<alpha> l)
[PROOF STEP]
apply (drule cnv_to_ufa_\<alpha>_eq, simp_all)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2 l szl l' l'a a b aa ba. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l'; ufa_invar l'; ufa_invar l'a; length l' = length l; length l'a = length l; \<forall>i<length l. rep_of l'a i = rep_of l i; (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl; (aa, ba) \<in> ufa_\<alpha> l'a; ufa_\<alpha> l = ufa_\<alpha> l'\<rbrakk> \<Longrightarrow> (aa, ba) \<in> ufa_\<alpha> l'
 2. \<And>x1 x2 l szl l' l'a a b aa ba. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l; ufa_invar l'; ufa_invar l'a; length l' = length l; \<forall>i<length l. rep_of l' i = rep_of l i; length l'a = length l; \<forall>i<length l. rep_of l'a i = rep_of l i; (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl; (aa, ba) \<in> ufa_\<alpha> l\<rbrakk> \<Longrightarrow> (aa, ba) \<in> ufa_\<alpha> l'a
 3. \<And>x1 x2 l szl l' l'a. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l; ufa_invar l'; ufa_invar l'a; length l' = length l; \<forall>i<length l. rep_of l' i = rep_of l i; length l'a = length l; \<forall>i<length l. rep_of l'a i = rep_of l i; \<exists>a b. (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl\<rbrakk> \<Longrightarrow> (rep_of l i = rep_of l j) = ((i, j) \<in> ufa_\<alpha> l)
[PROOF STEP]
apply (drule cnv_to_ufa_\<alpha>_eq, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 l szl l' l'a a b aa ba. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l; ufa_invar l'; ufa_invar l'a; length l' = length l; \<forall>i<length l. rep_of l' i = rep_of l i; length l'a = length l; \<forall>i<length l. rep_of l'a i = rep_of l i; (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl; (aa, ba) \<in> ufa_\<alpha> l\<rbrakk> \<Longrightarrow> (aa, ba) \<in> ufa_\<alpha> l'a
 2. \<And>x1 x2 l szl l' l'a. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l; ufa_invar l'; ufa_invar l'a; length l' = length l; \<forall>i<length l. rep_of l' i = rep_of l i; length l'a = length l; \<forall>i<length l. rep_of l'a i = rep_of l i; \<exists>a b. (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl\<rbrakk> \<Longrightarrow> (rep_of l i = rep_of l j) = ((i, j) \<in> ufa_\<alpha> l)
[PROOF STEP]
apply (drule cnv_to_ufa_\<alpha>_eq, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 l szl l' l'a a b aa ba. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l'; ufa_invar l'; ufa_invar l'a; length l' = length l; length l'a = length l; \<forall>i<length l. rep_of l'a i = rep_of l i; (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl; (aa, ba) \<in> ufa_\<alpha> l'; ufa_\<alpha> l = ufa_\<alpha> l'\<rbrakk> \<Longrightarrow> (aa, ba) \<in> ufa_\<alpha> l'a
 2. \<And>x1 x2 l szl l' l'a. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l; ufa_invar l'; ufa_invar l'a; length l' = length l; \<forall>i<length l. rep_of l' i = rep_of l i; length l'a = length l; \<forall>i<length l. rep_of l'a i = rep_of l i; \<exists>a b. (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl\<rbrakk> \<Longrightarrow> (rep_of l i = rep_of l j) = ((i, j) \<in> ufa_\<alpha> l)
[PROOF STEP]
apply (drule cnv_to_ufa_\<alpha>_eq, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 l szl l' l'a. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l; ufa_invar l'; ufa_invar l'a; length l' = length l; \<forall>i<length l. rep_of l' i = rep_of l i; length l'a = length l; \<forall>i<length l. rep_of l'a i = rep_of l i; \<exists>a b. (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl\<rbrakk> \<Longrightarrow> (rep_of l i = rep_of l j) = ((i, j) \<in> ufa_\<alpha> l)
[PROOF STEP]
apply (drule cnv_to_ufa_\<alpha>_eq, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 l szl l' l'a. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l'; ufa_invar l'; ufa_invar l'a; length l' = length l; length l'a = length l; \<forall>i<length l. rep_of l'a i = rep_of l i; \<exists>a b. (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl; ufa_\<alpha> l = ufa_\<alpha> l'\<rbrakk> \<Longrightarrow> (rep_of l i = rep_of l j) = ((i, j) \<in> ufa_\<alpha> l')
[PROOF STEP]
apply (drule cnv_to_ufa_\<alpha>_eq, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 l szl l' l'a. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l'; ufa_invar l'; ufa_invar l'a; length l' = length l; length l'a = length l; \<exists>a b. (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl; ufa_\<alpha> l'a = ufa_\<alpha> l'; ufa_\<alpha> l = ufa_\<alpha> l'\<rbrakk> \<Longrightarrow> (rep_of l i = rep_of l j) = ((i, j) \<in> ufa_\<alpha> l')
[PROOF STEP]
apply (subst ufa_find_correct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 l szl l' l'a. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l'; ufa_invar l'; ufa_invar l'a; length l' = length l; length l'a = length l; \<exists>a b. (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl; ufa_\<alpha> l'a = ufa_\<alpha> l'; ufa_\<alpha> l = ufa_\<alpha> l'\<rbrakk> \<Longrightarrow> ufa_invar l
 2. \<And>x1 x2 l szl l' l'a. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l'; ufa_invar l'; ufa_invar l'a; length l' = length l; length l'a = length l; \<exists>a b. (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl; ufa_\<alpha> l'a = ufa_\<alpha> l'; ufa_\<alpha> l = ufa_\<alpha> l'\<rbrakk> \<Longrightarrow> i < length l
 3. \<And>x1 x2 l szl l' l'a. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l'; ufa_invar l'; ufa_invar l'a; length l' = length l; length l'a = length l; \<exists>a b. (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl; ufa_\<alpha> l'a = ufa_\<alpha> l'; ufa_\<alpha> l = ufa_\<alpha> l'\<rbrakk> \<Longrightarrow> j < length l
 4. \<And>x1 x2 l szl l' l'a. \<lbrakk>u = (x1, x2); ufa_invar l; i < length l; j < length l; length szl = length l; R = ufa_\<alpha> l'; ufa_invar l'; ufa_invar l'a; length l' = length l; length l'a = length l; \<exists>a b. (a, b) \<Turnstile> x2 \<mapsto>\<^sub>a l'a * x1 \<mapsto>\<^sub>a szl; ufa_\<alpha> l'a = ufa_\<alpha> l'; ufa_\<alpha> l = ufa_\<alpha> l'\<rbrakk> \<Longrightarrow> ((i, j) \<in> ufa_\<alpha> l) = ((i, j) \<in> ufa_\<alpha> l')
[PROOF STEP]
apply (auto simp add: )
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma uf_union_rule[sep_heap_rules]: "\<lbrakk>i\<in>Domain R; j\<in> Domain R\<rbrakk>
  \<Longrightarrow> <is_uf R u> uf_union u i j <is_uf (per_union R i j)>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> Domain R; j \<in> Domain R\<rbrakk> \<Longrightarrow> <is_uf R u> uf_union u i j <is_uf (per_union R i j)>
[PROOF STEP]
unfolding uf_union_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> Domain R; j \<in> Domain R\<rbrakk> \<Longrightarrow> <is_uf R u> let (s, p) = u in uf_rep_of p i \<bind> (\<lambda>ci. uf_rep_of p j \<bind> (\<lambda>cj. if ci = cj then return (s, p) else Array.nth s ci \<bind> (\<lambda>si. Array.nth s cj \<bind> (\<lambda>sj. if si < sj then Array.upd ci cj p \<bind> (\<lambda>_. Array.upd cj (si + sj) s \<bind> (\<lambda>_. return (s, p))) else Array.upd cj ci p \<bind> (\<lambda>_. Array.upd ci (si + sj) s \<bind> (\<lambda>_. return (s, p))))))) <is_uf (per_union R i j)>
[PROOF STEP]
apply (cases u)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>i \<in> Domain R; j \<in> Domain R; u = (a, b)\<rbrakk> \<Longrightarrow> <is_uf R u> let (s, p) = u in uf_rep_of p i \<bind> (\<lambda>ci. uf_rep_of p j \<bind> (\<lambda>cj. if ci = cj then return (s, p) else Array.nth s ci \<bind> (\<lambda>si. Array.nth s cj \<bind> (\<lambda>sj. if si < sj then Array.upd ci cj p \<bind> (\<lambda>_. Array.upd cj (si + sj) s \<bind> (\<lambda>_. return (s, p))) else Array.upd cj ci p \<bind> (\<lambda>_. Array.upd ci (si + sj) s \<bind> (\<lambda>_. return (s, p))))))) <is_uf (per_union R i j)>
[PROOF STEP]
apply (simp add: is_uf_def[abs_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>i \<in> Domain R; j \<in> Domain R; u = (a, b)\<rbrakk> \<Longrightarrow> <\<exists>\<^sub>Al szl. b \<mapsto>\<^sub>a l * a \<mapsto>\<^sub>a szl * \<up> (ufa_invar l \<and> ufa_\<alpha> l = R \<and> length szl = length l)> uf_rep_of b i \<bind> (\<lambda>ci. uf_rep_of b j \<bind> (\<lambda>cj. if ci = cj then return (a, b) else Array.nth a ci \<bind> (\<lambda>si. Array.nth a cj \<bind> (\<lambda>sj. if si < sj then Array.upd ci cj b \<bind> (\<lambda>_. Array.upd cj (si + sj) a \<bind> (\<lambda>_. return (a, b))) else Array.upd cj ci b \<bind> (\<lambda>_. Array.upd ci (si + sj) a \<bind> (\<lambda>_. return (a, b))))))) <\<lambda>(s, p). \<exists>\<^sub>Al szl. p \<mapsto>\<^sub>a l * s \<mapsto>\<^sub>a szl * \<up> (ufa_invar l \<and> ufa_\<alpha> l = per_union R i j \<and> length szl = length l)>
[PROOF STEP]
apply (sep_auto
    simp: per_union_cmp ufa_\<alpha>_lenD ufa_find_correct
    rep_of_bound
    ufa_union_invar
    ufa_union_correct
  )
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done