theory Deterministic_AI

lemma cap_move_valid_list [wp]:

  notes split_paired_All[simp del] if_weak_cong[cong]
  shows
  "\<lbrace>valid_list\<rbrace>
  cap_move cap src dest
  \<lbrace>\<lambda>_. valid_list\<rbrace>" apply (case_tac "src = dest") apply (simp add: cap_move_def) apply(simp add: set_cdt_def cap_move_ext_def
                    update_cdt_list_def set_cdt_list_def del: fun_upd_apply split del: if_split) apply(wp) apply (simp del: fun_upd_apply cong: option.case_cong) apply (wp set_cap_caps_of_state3)+ apply (case_tac "cdt s dest") apply (fastforce simp: valid_list_2_def list_remove_removed intro: list_remove_distinct)+ apply (simp add: cap_move_def) apply(simp add: cap_move_def set_cdt_def cap_move_ext_def bind_assoc
                  update_cdt_list_def set_cdt_list_def del: fun_upd_apply split del: if_split) apply(wp) apply (simp del: fun_upd_apply split del: if_split) apply (wp set_cap_caps_of_state3)+ apply (rule mdb_move_abs_simple.valid_list_post) apply (rule mdb_move_abs_simple.intro; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (2 subgoals):
 1. src = dest \<Longrightarrow> \<lbrace>valid_list\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. valid_list\<rbrace>
 2. src \<noteq> dest \<Longrightarrow> \<lbrace>valid_list\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (2 subgoals):
 1. src = dest \<Longrightarrow> \<lbrace>valid_list\<rbrace> do y <- set_cap cap dest;
y <- set_cap NullCap dest;
src_p <- gets (\<lambda>s. cdt s dest);
dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
y <- set_cdt (cdt(dest := None));
y <- cap_move_ext dest dest src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original dest (is_original dest);
set_original dest False
od \<lbrace>\<lambda>_. valid_list\<rbrace>
 2. src \<noteq> dest \<Longrightarrow> \<lbrace>valid_list\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (2 subgoals):
 1. src = dest \<Longrightarrow> \<lbrace>valid_list\<rbrace> do y <- set_cap cap dest;
y <- set_cap NullCap dest;
src_p <- gets (\<lambda>s. cdt s dest);
dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
y <- do s <- get;
put (s\<lparr>cdt := cdt(dest := None)\<rparr>)
od;
y <- do t <- gets cdt_list;
s <- get;
put (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> t | Some p \<Rightarrow> t(p := list_remove (t p) dest)) s)
od;
is_original <- gets is_original_cap;
y <- set_original dest (is_original dest);
set_original dest False
od \<lbrace>\<lambda>_. valid_list\<rbrace>
 2. src \<noteq> dest \<Longrightarrow> \<lbrace>valid_list\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>y. src = dest \<Longrightarrow> \<lbrace>?B4 y\<rbrace> set_cap NullCap dest \<lbrace>\<lambda>ya s. valid_list (s\<lparr>cdt := (cdt s)(dest := None), cdt_list := case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>) p) dest), is_original_cap := (is_original_cap (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>) p) dest)) (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>)))(dest := is_original_cap (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>) p) dest)) (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>)) dest), is_original_cap := (is_original_cap (s\<lparr>cdt := (cdt s)(dest := None), cdt_list := case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>) p) dest), is_original_cap := (is_original_cap (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>) p) dest)) (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>)))(dest := is_original_cap (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>) p) dest)) (s\<lparr>cdt := (cdt s)(dest := None)\<rparr>)) dest)\<rparr>))(dest := False)\<rparr>)\<rbrace>
 2. src = dest \<Longrightarrow> \<lbrace>?Q3\<rbrace> set_cap cap dest \<lbrace>?B4\<rbrace>
 3. \<And>s. \<lbrakk>src = dest; valid_list s\<rbrakk> \<Longrightarrow> ?Q3 s
 4. src \<noteq> dest \<Longrightarrow> \<lbrace>valid_list\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (4 subgoals):
 1. src = dest \<Longrightarrow> \<lbrace>?B4 ()\<rbrace> set_cap NullCap dest \<lbrace>\<lambda>ya s. valid_list_2 (case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) ((cdt s)(dest := None))\<rbrace>
 2. src = dest \<Longrightarrow> \<lbrace>?Q3\<rbrace> set_cap cap dest \<lbrace>?B4\<rbrace>
 3. \<And>s. \<lbrakk>src = dest; valid_list s\<rbrakk> \<Longrightarrow> ?Q3 s
 4. src \<noteq> dest \<Longrightarrow> \<lbrace>valid_list\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>src = dest; valid_list s\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) ((cdt s)(dest := None))
 2. src \<noteq> dest \<Longrightarrow> \<lbrace>valid_list\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>src = dest; valid_list s; cdt s dest = None\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) ((cdt s)(dest := None))
 2. \<And>s a. \<lbrakk>src = dest; valid_list s; cdt s dest = Some a\<rbrakk> \<Longrightarrow> valid_list_2 (case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) ((cdt s)(dest := None))
 3. src \<noteq> dest \<Longrightarrow> \<lbrace>valid_list\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. src \<noteq> dest \<Longrightarrow> \<lbrace>valid_list\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. src \<noteq> dest \<Longrightarrow> \<lbrace>valid_list\<rbrace> do y <- set_cap cap dest;
y <- set_cap NullCap src;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (if r = src then None else (cdt(dest := cdt src)) r) = Some src then Some dest else (cdt(dest := cdt src, src := None)) r);
y <- cap_move_ext src dest src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original dest (is_original src);
set_original src False
od \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. src \<noteq> dest \<Longrightarrow> \<lbrace>valid_list\<rbrace> do y <- set_cap cap dest;
y <- set_cap NullCap src;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
x <- get;
y <- put (x\<lparr>cdt := \<lambda>r. if (if r = src then None else (cdt(dest := cdt src)) r) = Some src then Some dest else (cdt(dest := cdt src, src := None)) r\<rparr>);
x <- gets cdt_list;
xa <- get;
x <- put (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> x | Some p \<Rightarrow> x(p := list_remove (x p) dest)) xa);
x <- gets cdt_list;
xa <- get;
x <- put (cdt_list_update (\<lambda>_. case src_p of None \<Rightarrow> x | Some p \<Rightarrow> x(p := list_replace (x p) src dest)) xa);
x <- gets cdt_list;
xa <- get;
y <- put (cdt_list_update (\<lambda>_. x(src := [], dest := x src @ x dest)) xa);
is_original <- gets is_original_cap;
y <- set_original dest (is_original src);
set_original src False
od \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y. src \<noteq> dest \<Longrightarrow> \<lbrace>?B143 y\<rbrace> set_cap NullCap src \<lbrace>\<lambda>ya s. valid_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r, cdt_list := case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest), cdt_list := case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest), cdt_list := (cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))))(src := [], dest := cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))) src @ cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))) dest), is_original_cap := (is_original_cap (cdt_list_update (\<lambda>_. (cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))))(src := [], dest := cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))) src @ cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))) dest)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))))(dest := is_original_cap (cdt_list_update (\<lambda>_. (cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))))(src := [], dest := cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))) src @ cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))) dest)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))) src), is_original_cap := (is_original_cap (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r, cdt_list := case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest), cdt_list := case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest), cdt_list := (cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))))(src := [], dest := cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))) src @ cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))) dest), is_original_cap := (is_original_cap (cdt_list_update (\<lambda>_. (cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))))(src := [], dest := cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))) src @ cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))) dest)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))))(dest := is_original_cap (cdt_list_update (\<lambda>_. (cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))))(src := [], dest := cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))) src @ cdt_list (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))) dest)) (cdt_list_update (\<lambda>_. case cdt s src of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))(p := list_replace (cdt_list (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)) p) src dest)) (cdt_list_update (\<lambda>_. case cdt s dest of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>) p) dest)) (s\<lparr>cdt := \<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r\<rparr>)))) src)\<rparr>))(src := False)\<rparr>)\<rbrace>
 2. src \<noteq> dest \<Longrightarrow> \<lbrace>?Q142\<rbrace> set_cap cap dest \<lbrace>?B143\<rbrace>
 3. \<And>s. \<lbrakk>src \<noteq> dest; valid_list s\<rbrakk> \<Longrightarrow> ?Q142 s proof (prove)
goal (3 subgoals):
 1. src \<noteq> dest \<Longrightarrow> \<lbrace>?B143 ()\<rbrace> set_cap NullCap src \<lbrace>\<lambda>ya s. valid_list_2 ((case cdt s src of None \<Rightarrow> case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest) | Some p \<Rightarrow> (case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest))(p := list_replace ((case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) p) src dest))(src := [], dest := (case cdt s src of None \<Rightarrow> case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest) | Some p \<Rightarrow> (case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest))(p := list_replace ((case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) p) src dest)) src @ (case cdt s src of None \<Rightarrow> case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest) | Some p \<Rightarrow> (case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest))(p := list_replace ((case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) p) src dest)) dest)) (\<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r)\<rbrace>
 2. src \<noteq> dest \<Longrightarrow> \<lbrace>?Q142\<rbrace> set_cap cap dest \<lbrace>?B143\<rbrace>
 3. \<And>s. \<lbrakk>src \<noteq> dest; valid_list s\<rbrakk> \<Longrightarrow> ?Q142 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>src \<noteq> dest; valid_list s\<rbrakk> \<Longrightarrow> valid_list_2 ((case cdt s src of None \<Rightarrow> case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest) | Some p \<Rightarrow> (case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest))(p := list_replace ((case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) p) src dest))(src := [], dest := (case cdt s src of None \<Rightarrow> case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest) | Some p \<Rightarrow> (case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest))(p := list_replace ((case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) p) src dest)) src @ (case cdt s src of None \<Rightarrow> case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest) | Some p \<Rightarrow> (case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest))(p := list_replace ((case cdt s dest of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) p) src dest)) dest)) (\<lambda>r. if (if r = src then None else ((cdt s)(dest := cdt s src)) r) = Some src then Some dest else ((cdt s)(dest := cdt s src, src := None)) r) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>src \<noteq> dest; valid_list s\<rbrakk> \<Longrightarrow> mdb_move_abs_simple (cdt s) (cdt_list s) src dest proof (prove)
goal:
No subgoals!