theory Detype_R

lemma locateCTE_commute:
  assumes nf: "no_fail P0 f" "no_fail P1 (locateCTE src)"
  and psp_distinct: "\<lbrace>\<lambda>s. P2 s \<rbrace> f \<lbrace>\<lambda>a s. pspace_distinct' s\<rbrace>"
  and psp_aligned: "\<lbrace>\<lambda>s. P3 s \<rbrace> f \<lbrace>\<lambda>a s. pspace_aligned' s\<rbrace>"
  assumes ko_wp_at: "\<And>Q dest.
  \<lbrace>\<lambda>s. (P0 and P1 and P2 and P3) s  \<and> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj))  dest s \<rbrace> f
  \<lbrace>\<lambda>a s. ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest s\<rbrace>"
  and cte_wp_at: "\<And> dest.
  \<lbrace>\<lambda>s. (P0 and P1 and P2 and P3) s \<and> cte_wp_at' \<top> dest s \<rbrace> f
  \<lbrace>\<lambda>a s. cte_wp_at' \<top> dest s\<rbrace>"
  shows "monad_commute (P0 and P1 and P2 and P3 and P4 and P5 and pspace_aligned' and pspace_distinct')
  (locateCTE src) f" proof - have same:
    "\<And>ptr val next s s'. (ptr, s') \<in> fst (locateCTE src s)
    \<Longrightarrow> s' = s" by (erule use_valid[OF _ locateCTE_inv],simp) show ?thesis apply (clarsimp simp:monad_commute_def) apply (clarsimp simp:bind_def return_def) apply (intro conjI iffI set_eqI) apply (clarsimp) apply (frule same) apply (clarsimp) apply (rule bexI[rotated], assumption) apply (frule singleton_locateCTE[THEN iffD1]) apply (frule locateCTE_monad [OF ko_wp_at cte_wp_at psp_distinct psp_aligned]) apply assumption+ apply simp apply (clarsimp) apply (rule bexI[rotated]) apply (fastforce) apply clarsimp apply clarsimp apply (frule empty_failD2[OF empty_fail_locateCTE no_failD[OF nf(2)]]) apply clarsimp apply (rule bexI[rotated],assumption) apply (clarsimp) apply (frule_tac s = bb in same) apply (frule_tac s = s in same) apply clarsimp apply (frule_tac s1 = s in singleton_locateCTE[THEN iffD1]) apply (frule locateCTE_monad [OF ko_wp_at cte_wp_at psp_distinct psp_aligned]) apply assumption+ apply simp apply (rule bexI[rotated],assumption) apply (drule sym) apply (clarsimp simp:singleton_locateCTE singleton_iff) apply fastforce apply (clarsimp simp:split_def image_def) apply (elim disjE) apply clarsimp apply (drule same) apply simp apply (frule no_failD[OF nf(2)]) apply simp apply (clarsimp simp:split_def image_def) apply (elim disjE) apply clarsimp apply (frule empty_failD2[OF empty_fail_locateCTE no_failD[OF nf(2)]]) apply clarsimp apply (frule same) apply simp apply (frule singleton_locateCTE[THEN iffD1]) apply (frule locateCTE_monad [OF ko_wp_at cte_wp_at psp_distinct psp_aligned]) apply assumption+ apply simp apply (clarsimp) apply (simp add: fail_empty_locateCTE) apply (simp add: no_failD[OF nf(1)]) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (P0 and P1 and P2 and P3 and P4 and P5 and pspace_aligned' and pspace_distinct') (locateCTE src) f proof (state)
goal (1 subgoal):
 1. monad_commute (P0 and P1 and P2 and P3 and P4 and P5 and pspace_aligned' and pspace_distinct') (locateCTE src) f proof (prove)
goal (1 subgoal):
 1. \<And>ptr val next s s'. (ptr, s') \<in> fst (locateCTE src s) \<Longrightarrow> s' = s proof (state)
this:
(?ptr, ?s') \<in> fst (locateCTE src ?s) \<Longrightarrow> ?s' = ?s

goal (1 subgoal):
 1. monad_commute (P0 and P1 and P2 and P3 and P4 and P5 and pspace_aligned' and pspace_distinct') (locateCTE src) f proof (prove)
goal (1 subgoal):
 1. monad_commute (P0 and P1 and P2 and P3 and P4 and P5 and pspace_aligned' and pspace_distinct') (locateCTE src) f proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> (do x <- locateCTE src;
y <- f;
return (x, y)
od) s = (do y <- f;
x <- locateCTE src;
return (x, y)
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) = (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<and> ((\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)) = ((\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)) proof (prove)
goal (4 subgoals):
 1. \<And>s x. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; x \<in> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s))))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s))))
 2. \<And>s x. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; x \<in> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s))))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s))))
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 4. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (4 subgoals):
 1. \<And>s b ba aa bb. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f bb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). ((aa, b), ba) \<in> fst (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))
 2. \<And>s x. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; x \<in> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s))))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s))))
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 4. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (4 subgoals):
 1. \<And>s b ba aa bb. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f bb); bb = s\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). ((aa, b), ba) \<in> fst (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))
 2. \<And>s x. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; x \<in> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s))))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s))))
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 4. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (4 subgoals):
 1. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). ((aa, b), ba) \<in> fst (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))
 2. \<And>s x. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; x \<in> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s))))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s))))
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 4. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (4 subgoals):
 1. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s)\<rbrakk> \<Longrightarrow> ((aa, b), ba) \<in> fst (case (b, ba) of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))
 2. \<And>s x. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; x \<in> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s))))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s))))
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 4. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (4 subgoals):
 1. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s); {(aa, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> ((aa, b), ba) \<in> fst (case (b, ba) of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))
 2. \<And>s x. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; x \<in> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s))))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s))))
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 4. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (8 subgoals):
 1. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s); {(aa, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> (?r36 s b ba aa, ?s'36 s b ba aa) \<in> fst (f s)
 2. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s); {(aa, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> pspace_aligned' s
 3. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s); {(aa, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> pspace_distinct' s
 4. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s); {(aa, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> (P0 and P1 and P2 and P3 and (P0 and P1 and P2 and P3) and P2 and P3) s
 5. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s); {(aa, s)} = fst (locateCTE src s); {(aa, ?s'36 s b ba aa)} = fst (locateCTE src (?s'36 s b ba aa))\<rbrakk> \<Longrightarrow> ((aa, b), ba) \<in> fst (case (b, ba) of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))
 6. \<And>s x. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; x \<in> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s))))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s))))
 7. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 8. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (5 subgoals):
 1. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s); {(aa, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> (P0 and P1 and P2 and P3 and (P0 and P1 and P2 and P3) and P2 and P3) s
 2. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s); {(aa, s)} = fst (locateCTE src s); {(aa, ba)} = fst (locateCTE src ba)\<rbrakk> \<Longrightarrow> ((aa, b), ba) \<in> fst (case (b, ba) of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))
 3. \<And>s x. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; x \<in> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s))))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s))))
 4. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 5. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (4 subgoals):
 1. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s); {(aa, s)} = fst (locateCTE src s); {(aa, ba)} = fst (locateCTE src ba)\<rbrakk> \<Longrightarrow> ((aa, b), ba) \<in> fst (case (b, ba) of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))
 2. \<And>s x. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; x \<in> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s))))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s))))
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 4. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (4 subgoals):
 1. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s); {(aa, s)} = fst (locateCTE src s); {(aa, ba)} = fst (locateCTE src ba)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src ba). ((aa, b), ba) \<in> fst (case x of (x, s) \<Rightarrow> ({((x, b), s)}, False))
 2. \<And>s x. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; x \<in> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s))))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s))))
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 4. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (5 subgoals):
 1. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s); {(aa, s)} = fst (locateCTE src s); {(aa, ba)} = fst (locateCTE src ba)\<rbrakk> \<Longrightarrow> ?x44 s b ba aa \<in> fst (locateCTE src ba)
 2. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s); {(aa, s)} = fst (locateCTE src s); {(aa, ba)} = fst (locateCTE src ba)\<rbrakk> \<Longrightarrow> ((aa, b), ba) \<in> fst (case ?x44 s b ba aa of (x, s) \<Rightarrow> ({((x, b), s)}, False))
 3. \<And>s x. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; x \<in> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s))))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s))))
 4. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 5. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (4 subgoals):
 1. \<And>s b ba aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, s) \<in> fst (locateCTE src s); (b, ba) \<in> fst (f s); {(aa, s)} = fst (locateCTE src s); {(aa, ba)} = fst (locateCTE src ba)\<rbrakk> \<Longrightarrow> ((aa, b), ba) \<in> fst (case (aa, ba) of (x, s) \<Rightarrow> ({((x, b), s)}, False))
 2. \<And>s x. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; x \<in> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s))))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s))))
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 4. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; x \<in> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s))))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s))))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a ba aa bb. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, ba) \<in> fst (locateCTE src bb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). ((a, aa), ba) \<in> fst (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a ba aa bb. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, ba) \<in> fst (locateCTE src bb); \<exists>v. v \<in> fst (locateCTE src s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). ((a, aa), ba) \<in> fst (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a ba aa bb ab b. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, ba) \<in> fst (locateCTE src bb); (ab, b) \<in> fst (locateCTE src s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). ((a, aa), ba) \<in> fst (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a ba aa bb ab b. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, ba) \<in> fst (locateCTE src bb); (ab, b) \<in> fst (locateCTE src s)\<rbrakk> \<Longrightarrow> ((a, aa), ba) \<in> fst (case (ab, b) of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a ba aa bb ab b. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, ba) \<in> fst (locateCTE src bb); (ab, b) \<in> fst (locateCTE src s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f b). ((a, aa), ba) \<in> fst (case x of (y, s) \<Rightarrow> ({((ab, y), s)}, False))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a ba aa bb ab b. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, ba) \<in> fst (locateCTE src bb); (ab, b) \<in> fst (locateCTE src s); ba = bb\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f b). ((a, aa), ba) \<in> fst (case x of (y, s) \<Rightarrow> ({((ab, y), s)}, False))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a ba aa bb ab b. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, ba) \<in> fst (locateCTE src bb); (ab, b) \<in> fst (locateCTE src s); ba = bb; b = s\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f b). ((a, aa), ba) \<in> fst (case x of (y, s) \<Rightarrow> ({((ab, y), s)}, False))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a aa bb ab. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, bb) \<in> fst (locateCTE src bb); (ab, s) \<in> fst (locateCTE src s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). ((a, aa), bb) \<in> fst (case x of (y, s) \<Rightarrow> ({((ab, y), s)}, False))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a aa bb ab. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, bb) \<in> fst (locateCTE src bb); (ab, s) \<in> fst (locateCTE src s); {(ab, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). ((a, aa), bb) \<in> fst (case x of (y, s) \<Rightarrow> ({((ab, y), s)}, False))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (7 subgoals):
 1. \<And>s a aa bb ab. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, bb) \<in> fst (locateCTE src bb); (ab, s) \<in> fst (locateCTE src s); {(ab, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> (?r93 s a aa bb ab, ?s'93 s a aa bb ab) \<in> fst (f s)
 2. \<And>s a aa bb ab. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, bb) \<in> fst (locateCTE src bb); (ab, s) \<in> fst (locateCTE src s); {(ab, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> pspace_aligned' s
 3. \<And>s a aa bb ab. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, bb) \<in> fst (locateCTE src bb); (ab, s) \<in> fst (locateCTE src s); {(ab, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> pspace_distinct' s
 4. \<And>s a aa bb ab. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, bb) \<in> fst (locateCTE src bb); (ab, s) \<in> fst (locateCTE src s); {(ab, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> (P0 and P1 and P2 and P3 and (P0 and P1 and P2 and P3) and P2 and P3) s
 5. \<And>s a aa bb ab. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, bb) \<in> fst (locateCTE src bb); (ab, s) \<in> fst (locateCTE src s); {(ab, s)} = fst (locateCTE src s); {(ab, ?s'93 s a aa bb ab)} = fst (locateCTE src (?s'93 s a aa bb ab))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). ((a, aa), bb) \<in> fst (case x of (y, s) \<Rightarrow> ({((ab, y), s)}, False))
 6. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 7. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (4 subgoals):
 1. \<And>s a aa bb ab. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, bb) \<in> fst (locateCTE src bb); (ab, s) \<in> fst (locateCTE src s); {(ab, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> (P0 and P1 and P2 and P3 and (P0 and P1 and P2 and P3) and P2 and P3) s
 2. \<And>s a aa bb ab. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, bb) \<in> fst (locateCTE src bb); (ab, s) \<in> fst (locateCTE src s); {(ab, s)} = fst (locateCTE src s); {(ab, bb)} = fst (locateCTE src bb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). ((a, aa), bb) \<in> fst (case x of (y, s) \<Rightarrow> ({((ab, y), s)}, False))
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 4. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a aa bb ab. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, bb) \<in> fst (locateCTE src bb); (ab, s) \<in> fst (locateCTE src s); {(ab, s)} = fst (locateCTE src s); {(ab, bb)} = fst (locateCTE src bb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). ((a, aa), bb) \<in> fst (case x of (y, s) \<Rightarrow> ({((ab, y), s)}, False))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a aa bb ab. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, bb) \<in> fst (locateCTE src bb); (ab, s) \<in> fst (locateCTE src s); {(ab, s)} = fst (locateCTE src s); {(ab, bb)} = fst (locateCTE src bb)\<rbrakk> \<Longrightarrow> ((a, aa), bb) \<in> fst (case (aa, bb) of (y, s) \<Rightarrow> ({((ab, y), s)}, False))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a aa bb ab. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); (a, bb) \<in> fst (locateCTE src bb); (ab, s) \<in> fst (locateCTE src s); {(ab, bb)} = fst (locateCTE src bb); fst (locateCTE src s) = {(ab, s)}\<rbrakk> \<Longrightarrow> ((a, aa), bb) \<in> fst (case (aa, bb) of (y, s) \<Rightarrow> ({((ab, y), s)}, False))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a aa bb ab. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (aa, bb) \<in> fst (f s); {(a, bb)} = fst (locateCTE src bb); {(ab, bb)} = fst (locateCTE src bb); fst (locateCTE src s) = {(ab, s)}\<rbrakk> \<Longrightarrow> a = ab
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (locateCTE src s). snd (f (snd x))) \<or> snd (locateCTE src s); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). snd (locateCTE src (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (f s); \<exists>x\<in>fst (locateCTE src s). snd (f (snd x))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). snd (locateCTE src (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (f s); snd (locateCTE src s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). snd (locateCTE src (snd x))
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (f s); (a, b) \<in> fst (locateCTE src s); snd (f b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). snd (locateCTE src (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (f s); snd (locateCTE src s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). snd (locateCTE src (snd x))
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (f s); snd (f b); b = s\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). snd (locateCTE src (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (f s); snd (locateCTE src s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). snd (locateCTE src (snd x))
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (f s); snd (locateCTE src s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). snd (locateCTE src (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (f s); snd (locateCTE src s); \<not> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). snd (locateCTE src (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (case x of (y, s) \<Rightarrow> (\<Union>a\<in>fst (locateCTE src s). fst (case a of (x, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (locateCTE src s)))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (locateCTE src s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (f s). fst (case a of (y, s) \<Rightarrow> ({((x, y), s)}, False)), (\<exists>xa\<in>fst (f s). snd (case xa of (y, s) \<Rightarrow> ({((x, y), s)}, False))) \<or> snd (f s)))) \<or> snd (locateCTE src s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; (\<exists>x\<in>fst (f s). snd (locateCTE src (snd x))) \<or> snd (f s); \<not> snd (locateCTE src s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); \<exists>x\<in>fst (f s). snd (locateCTE src (snd x))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); snd (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); snd (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b); \<exists>v. v \<in> fst (locateCTE src s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); snd (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b); (aa, ba) \<in> fst (locateCTE src s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); snd (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b); (aa, ba) \<in> fst (locateCTE src s); ba = s\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); snd (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b); (aa, s) \<in> fst (locateCTE src s); ba = s\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); snd (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b); (aa, s) \<in> fst (locateCTE src s); ba = s; {(aa, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); snd (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x)) proof (prove)
goal (6 subgoals):
 1. \<And>s a b aa ba. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b); (aa, s) \<in> fst (locateCTE src s); ba = s; {(aa, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> (?r153 s a b aa ba, ?s'153 s a b aa ba) \<in> fst (f s)
 2. \<And>s a b aa ba. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b); (aa, s) \<in> fst (locateCTE src s); ba = s; {(aa, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> pspace_aligned' s
 3. \<And>s a b aa ba. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b); (aa, s) \<in> fst (locateCTE src s); ba = s; {(aa, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> pspace_distinct' s
 4. \<And>s a b aa ba. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b); (aa, s) \<in> fst (locateCTE src s); ba = s; {(aa, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> (P0 and P1 and P2 and P3 and (P0 and P1 and P2 and P3) and P2 and P3) s
 5. \<And>s a b aa ba. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b); (aa, s) \<in> fst (locateCTE src s); ba = s; {(aa, s)} = fst (locateCTE src s); {(aa, ?s'153 s a b aa ba)} = fst (locateCTE src (?s'153 s a b aa ba))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x))
 6. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); snd (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x)) proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b); (aa, s) \<in> fst (locateCTE src s); ba = s; {(aa, s)} = fst (locateCTE src s)\<rbrakk> \<Longrightarrow> (P0 and P1 and P2 and P3 and (P0 and P1 and P2 and P3) and P2 and P3) s
 2. \<And>s a b aa ba. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b); (aa, s) \<in> fst (locateCTE src s); ba = s; {(aa, s)} = fst (locateCTE src s); {(aa, b)} = fst (locateCTE src b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x))
 3. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); snd (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b); (aa, s) \<in> fst (locateCTE src s); ba = s; {(aa, s)} = fst (locateCTE src s); {(aa, b)} = fst (locateCTE src b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); snd (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); (a, b) \<in> fst (f s); snd (locateCTE src b); (aa, s) \<in> fst (locateCTE src s); {(aa, s)} = fst (locateCTE src s); {(aa, b)} = fst (locateCTE src b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x))
 2. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); snd (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P0 s; P1 s; P2 s; P3 s; P4 s; P5 s; pspace_aligned' s; pspace_distinct' s; \<not> snd (locateCTE src s); snd (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (locateCTE src s). snd (f (snd x)) proof (prove)
goal:
No subgoals! proof (state)
this:
monad_commute (P0 and P1 and P2 and P3 and P4 and P5 and pspace_aligned' and pspace_distinct') (locateCTE src) f

goal:
No subgoals!