theory Deterministic_AI

lemma cap_swap_valid_list [wp]:
  "\<lbrace>valid_list\<rbrace>
  cap_swap c a c' b
  \<lbrace>\<lambda>_. valid_list\<rbrace>" apply (simp only: cap_swap_def cap_swap_ext_extended.dxo_eq) apply (simp only: cap_swap_ext_def update_cdt_list_def set_cdt_list_def set_cdt_def bind_assoc) apply wp apply (simp del: fun_upd_apply split del: if_split cong: option.case_cong) apply (wp set_cap_caps_of_state3)+ apply (case_tac "a = b") apply (simp split: option.splits) apply(subgoal_tac "mdb_swap_abs_simple (cdt s) (cdt_list s)") prefer 2 apply(rule mdb_swap_abs_simple.intro) apply simp apply(frule mdb_swap_abs_simple.valid_list_post[where src=a and dest=b]) apply(simp add: fun_upd_def split del: if_split cong: option.case_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> do set_cap c' a;
set_cap c b;
slot1_p <- gets (\<lambda>s. cdt s a);
slot2_p <- gets (\<lambda>s. cdt s b);
cdt <- gets cdt;
cdt' <- return (\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n);
set_cdt (cdt'(a := cdt' b, b := cdt' a));
cap_swap_ext a b slot1_p slot2_p;
is_original <- gets is_original_cap;
set_original a (is_original b);
set_original b (is_original a)
od \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> do set_cap c' a;
set_cap c b;
slot1_p <- gets (\<lambda>s. cdt s a);
slot2_p <- gets (\<lambda>s. cdt s b);
cdt <- gets cdt;
cdt' <- return (\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n);
x <- get;
put $ x\<lparr>cdt := cdt'(a := cdt' b, b := cdt' a)\<rparr>;
x <- gets cdt_list;
xa <- get;
x <- put $ cdt_list_update (\<lambda>_. x(a := x b, b := x a)) xa;
K_bind (do t <- gets cdt_list;
s <- get;
put $ cdt_list_update (\<lambda>_. case if slot2_p = Some a then Some b else if slot2_p = Some b then Some a else slot2_p of None \<Rightarrow> case if slot1_p = Some a then Some b else if slot1_p = Some b then Some a else slot1_p of None \<Rightarrow> t | Some slot2_p \<Rightarrow> t(slot2_p := list_replace (t slot2_p) a b) | Some slot1_pa \<Rightarrow> case if slot1_p = Some a then Some b else if slot1_p = Some b then Some a else slot1_p of None \<Rightarrow> t(slot1_pa := list_replace (t slot1_pa) b a) | Some slot2_p \<Rightarrow> if slot1_pa = slot2_p then t(slot1_pa := list_swap (t slot1_pa) a b) else t(slot1_pa := list_replace (t slot1_pa) b a, slot2_p := list_replace (t slot2_p) a b)) s
od) x;
is_original <- gets is_original_cap;
set_original a (is_original b);
set_original b (is_original a)
od \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?B1 x\<rbrace> set_cap c b \<lbrace>\<lambda>xa s. valid_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a), cdt_list := (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a), cdt_list := case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) | Some slot2_p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_swap (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) a b) else (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) b a, slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot2_p) a b), is_original_cap := (is_original_cap (cdt_list_update (\<lambda>_. case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) | Some slot2_p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_swap (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) a b) else (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) b a, slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot2_p) a b)) (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))))(a := is_original_cap (cdt_list_update (\<lambda>_. case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) | Some slot2_p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_swap (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) a b) else (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) b a, slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot2_p) a b)) (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))) b), is_original_cap := (is_original_cap (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a), cdt_list := (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a), cdt_list := case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) | Some slot2_p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_swap (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) a b) else (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) b a, slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot2_p) a b), is_original_cap := (is_original_cap (cdt_list_update (\<lambda>_. case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) | Some slot2_p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_swap (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) a b) else (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) b a, slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot2_p) a b)) (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))))(a := is_original_cap (cdt_list_update (\<lambda>_. case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) | Some slot2_p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_swap (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) a b) else (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) b a, slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot2_p) a b)) (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))) b)\<rparr>))(b := is_original_cap (cdt_list_update (\<lambda>_. case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) | Some slot2_p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_swap (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) a b) else (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)))(slot1_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot1_p) b a, slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>)) slot2_p) a b)) (cdt_list_update (\<lambda>_. (cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))(a := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) b, b := cdt_list (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>) a)) (s\<lparr>cdt := (\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)\<rparr>))) a)\<rparr>)\<rbrace>
 2. \<lbrace>?Q\<rbrace> set_cap c' a \<lbrace>?B1\<rbrace>
 3. \<And>s. valid_list s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B1 ()\<rbrace> set_cap c b \<lbrace>\<lambda>xa s. valid_list_2 (case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a) | Some slot2_p \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_swap (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) else (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b)) ((\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a))\<rbrace>
 2. \<lbrace>?Q\<rbrace> set_cap c' a \<lbrace>?B1\<rbrace>
 3. \<And>s. valid_list s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_list s \<Longrightarrow> valid_list_2 (case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a) | Some slot2_p \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_swap (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) else (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b)) ((\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_list s; a = b\<rbrakk> \<Longrightarrow> valid_list_2 (case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a) | Some slot2_p \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_swap (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) else (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b)) ((\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a))
 2. \<And>s. \<lbrakk>valid_list s; a \<noteq> b\<rbrakk> \<Longrightarrow> valid_list_2 (case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a) | Some slot2_p \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_swap (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) else (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b)) ((\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_list s; a \<noteq> b\<rbrakk> \<Longrightarrow> valid_list_2 (case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a) | Some slot2_p \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_swap (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) else (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b)) ((\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_list s; a \<noteq> b; mdb_swap_abs_simple (cdt s) (cdt_list s)\<rbrakk> \<Longrightarrow> valid_list_2 (case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a) | Some slot2_p \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_swap (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) else (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b)) ((\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a))
 2. \<And>s. \<lbrakk>valid_list s; a \<noteq> b\<rbrakk> \<Longrightarrow> mdb_swap_abs_simple (cdt s) (cdt_list s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_list s; a \<noteq> b\<rbrakk> \<Longrightarrow> mdb_swap_abs_simple (cdt s) (cdt_list s)
 2. \<And>s. \<lbrakk>valid_list s; a \<noteq> b; mdb_swap_abs_simple (cdt s) (cdt_list s)\<rbrakk> \<Longrightarrow> valid_list_2 (case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a) | Some slot2_p \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_swap (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) else (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b)) ((\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_list s; a \<noteq> b\<rbrakk> \<Longrightarrow> valid_list s
 2. \<And>s. \<lbrakk>valid_list s; a \<noteq> b; mdb_swap_abs_simple (cdt s) (cdt_list s)\<rbrakk> \<Longrightarrow> valid_list_2 (case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a) | Some slot2_p \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_swap (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) else (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b)) ((\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_list s; a \<noteq> b; mdb_swap_abs_simple (cdt s) (cdt_list s)\<rbrakk> \<Longrightarrow> valid_list_2 (case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a) | Some slot2_p \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_swap (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) else (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b)) ((\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_list s; a \<noteq> b; mdb_swap_abs_simple (cdt s) (cdt_list s); valid_list_2 (case ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) a of None \<Rightarrow> case ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) b of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a) | Some dest_p \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, dest_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) dest_p) a b) | Some src_p \<Rightarrow> case ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) b of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, src_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) src_p) b a) | Some dest_p \<Rightarrow> if src_p = dest_p then (cdt_list s)(a := cdt_list s b, b := cdt_list s a, src_p := list_swap (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) src_p) a b) else (cdt_list s)(a := cdt_list s b, b := cdt_list s a, src_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) src_p) b a, dest_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) dest_p) a b)) ((\<lambda>n. if cdt s n = Some a then Some b else if cdt s n = Some b then Some a else cdt s n)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a))\<rbrakk> \<Longrightarrow> valid_list_2 (case if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b of None \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a) | Some slot2_p \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) | Some slot1_p \<Rightarrow> case if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a of None \<Rightarrow> (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a) | Some slot2_p \<Rightarrow> if slot1_p = slot2_p then (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot2_p := list_swap (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b) else (cdt_list s)(a := cdt_list s b, b := cdt_list s a, slot1_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot1_p) b a, slot2_p := list_replace (((cdt_list s)(a := cdt_list s b, b := cdt_list s a)) slot2_p) a b)) ((\<lambda>c. if cdt s c = Some a then Some b else if cdt s c = Some b then Some a else cdt s c)(a := if cdt s b = Some a then Some b else if cdt s b = Some b then Some a else cdt s b, b := if cdt s a = Some a then Some b else if cdt s a = Some b then Some a else cdt s a)) proof (prove)
goal:
No subgoals!