theory Deterministic_AI

lemma finite_depth:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "finite_depth n" apply (insert findepth) apply(simp add: finite_depth_def descendants split del: if_split) apply(simp add: n_def n'_def split del: if_split) apply(rule allI) apply(case_tac "slot=src") apply(erule_tac x=dest in allE) apply(elim exE conjE) apply(case_tac "p=src") apply(rule_tac x=dest in exI, simp add: s_d_swap_def) apply(case_tac "p = dest") apply(rule_tac x ="src" in exI, simp add: s_d_swap_def) apply(rule_tac x=p in exI, simp add: s_d_swap_def) apply (case_tac "slot=dest") apply(erule_tac x=src in allE) apply (elim exE conjE) apply (case_tac "p=src") apply (rule_tac x =dest in exI, simp add: s_d_swap_def) apply (case_tac "p=dest") apply (simp add: descendants_of_def) apply (intro conjI impI) apply (rule_tac x = "src" in exI, intro conjI, rule impI, simp+) apply (rule_tac x = "src" in exI) apply (intro conjI impI; simp) apply (rule_tac x = "p" in exI) apply (simp add: descendants_of_def s_d_swap_def) apply (erule_tac x = slot in allE) apply (elim exE conjE) apply (case_tac "p = dest") apply (rule_tac x = "src" in exI, simp add: descendants_of_def s_d_swap_def) apply (case_tac "p = src") apply (rule_tac x = "dest" in exI, simp add: descendants_of_def s_d_swap_def) apply (rule_tac x ="p" in exI, simp add: descendants_of_def s_d_swap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite_depth n proof (prove)
goal (1 subgoal):
 1. finite_depth m \<Longrightarrow> finite_depth n proof (prove)
goal (1 subgoal):
 1. \<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None \<Longrightarrow> \<forall>slot. \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> n p = None proof (prove)
goal (1 subgoal):
 1. \<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None \<Longrightarrow> \<forall>slot. \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot = src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>slot = src; \<exists>p. (dest \<in> descendants_of p m \<or> p = dest) \<and> m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot = src; dest \<in> descendants_of p m \<or> p = dest; m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot = src; dest \<in> descendants_of p m \<or> p = dest; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot p. \<lbrakk>slot = src; dest \<in> descendants_of p m \<or> p = dest; m p = None; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 3. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot = src; dest \<in> descendants_of p m \<or> p = dest; m p = None; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot = src; dest \<in> descendants_of p m \<or> p = dest; m p = None; p \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot p. \<lbrakk>slot = src; dest \<in> descendants_of p m \<or> p = dest; m p = None; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 3. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot = src; dest \<in> descendants_of p m \<or> p = dest; m p = None; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src; slot = dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>slot \<noteq> src; slot = dest; \<exists>p. (src \<in> descendants_of p m \<or> p = src) \<and> m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> src; slot = dest; src \<in> descendants_of p m \<or> p = src; m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> src; slot = dest; src \<in> descendants_of p m \<or> p = src; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot p. \<lbrakk>slot \<noteq> src; slot = dest; src \<in> descendants_of p m \<or> p = src; m p = None; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 3. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> src; slot = dest; src \<in> descendants_of p m \<or> p = src; m p = None; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> src; slot = dest; src \<in> descendants_of p m \<or> p = src; m p = None; p \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot p. \<lbrakk>slot \<noteq> src; slot = dest; src \<in> descendants_of p m \<or> p = src; m p = None; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 3. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m \<Turnstile> dest \<rightarrow> src; m dest = None; p = dest\<rbrakk> \<Longrightarrow> (m src = Some dest \<longrightarrow> (\<exists>p. (m \<Turnstile> s_d_swap p src dest \<rightarrow> src \<longrightarrow> (m p = Some dest \<longrightarrow> p = src) \<and> (m p \<noteq> Some dest \<longrightarrow> (m p = Some src \<longrightarrow> p = src) \<and> (m p \<noteq> Some src \<longrightarrow> p \<noteq> src \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> m p = None)))) \<and> ((s_d_swap p src dest, src) \<notin> (cdt_parent_rel m)\<^sup>+ \<longrightarrow> p = src))) \<and> (m src \<noteq> Some dest \<longrightarrow> (\<exists>p. (m \<Turnstile> s_d_swap p src dest \<rightarrow> src \<longrightarrow> (m p = Some dest \<longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> m src = None) \<and> p = dest) \<and> (m p \<noteq> Some dest \<longrightarrow> (m p = Some src \<longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> m src = None) \<and> p = dest) \<and> (m p \<noteq> Some src \<longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> m src = None) \<and> (p \<noteq> dest \<longrightarrow> m p = None)))) \<and> ((s_d_swap p src dest, src) \<notin> (cdt_parent_rel m)\<^sup>+ \<longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> m src = None) \<and> p = dest)))
 2. \<And>slot p. \<lbrakk>slot \<noteq> src; slot = dest; src \<in> descendants_of p m \<or> p = src; m p = None; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 3. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (4 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m \<Turnstile> dest \<rightarrow> src; m dest = None; p = dest; m src = Some dest\<rbrakk> \<Longrightarrow> \<exists>p. (m \<Turnstile> s_d_swap p src dest \<rightarrow> src \<longrightarrow> (m p = Some dest \<longrightarrow> p = src) \<and> (m p \<noteq> Some dest \<longrightarrow> (m p = Some src \<longrightarrow> p = src) \<and> (m p \<noteq> Some src \<longrightarrow> p \<noteq> src \<longrightarrow> p \<noteq> dest \<and> (p \<noteq> dest \<longrightarrow> m p = None)))) \<and> ((s_d_swap p src dest, src) \<notin> (cdt_parent_rel m)\<^sup>+ \<longrightarrow> p = src)
 2. \<And>slot p. \<lbrakk>slot = dest; m \<Turnstile> dest \<rightarrow> src; m dest = None; p = dest; m src \<noteq> Some dest\<rbrakk> \<Longrightarrow> \<exists>p. (m \<Turnstile> s_d_swap p src dest \<rightarrow> src \<longrightarrow> (m p = Some dest \<longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> m src = None) \<and> p = dest) \<and> (m p \<noteq> Some dest \<longrightarrow> (m p = Some src \<longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> m src = None) \<and> p = dest) \<and> (m p \<noteq> Some src \<longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> m src = None) \<and> (p \<noteq> dest \<longrightarrow> m p = None)))) \<and> ((s_d_swap p src dest, src) \<notin> (cdt_parent_rel m)\<^sup>+ \<longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> m src = None) \<and> p = dest)
 3. \<And>slot p. \<lbrakk>slot \<noteq> src; slot = dest; src \<in> descendants_of p m \<or> p = src; m p = None; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 4. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m \<Turnstile> dest \<rightarrow> src; m dest = None; p = dest; m src \<noteq> Some dest\<rbrakk> \<Longrightarrow> \<exists>p. (m \<Turnstile> s_d_swap p src dest \<rightarrow> src \<longrightarrow> (m p = Some dest \<longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> m src = None) \<and> p = dest) \<and> (m p \<noteq> Some dest \<longrightarrow> (m p = Some src \<longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> m src = None) \<and> p = dest) \<and> (m p \<noteq> Some src \<longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> m src = None) \<and> (p \<noteq> dest \<longrightarrow> m p = None)))) \<and> ((s_d_swap p src dest, src) \<notin> (cdt_parent_rel m)\<^sup>+ \<longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> m src = None) \<and> p = dest)
 2. \<And>slot p. \<lbrakk>slot \<noteq> src; slot = dest; src \<in> descendants_of p m \<or> p = src; m p = None; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 3. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m \<Turnstile> dest \<rightarrow> src; m dest = None; p = dest; m src \<noteq> Some dest\<rbrakk> \<Longrightarrow> (m \<Turnstile> s_d_swap src src dest \<rightarrow> src \<longrightarrow> (m src = Some dest \<longrightarrow> src \<noteq> src \<longrightarrow> (src = dest \<longrightarrow> m src = None) \<and> src = dest) \<and> (m src \<noteq> Some dest \<longrightarrow> (m src = Some src \<longrightarrow> src \<noteq> src \<longrightarrow> (src = dest \<longrightarrow> m src = None) \<and> src = dest) \<and> (m src \<noteq> Some src \<longrightarrow> src \<noteq> src \<longrightarrow> (src = dest \<longrightarrow> m src = None) \<and> (src \<noteq> dest \<longrightarrow> m src = None)))) \<and> ((s_d_swap src src dest, src) \<notin> (cdt_parent_rel m)\<^sup>+ \<longrightarrow> src \<noteq> src \<longrightarrow> (src = dest \<longrightarrow> m src = None) \<and> src = dest)
 2. \<And>slot p. \<lbrakk>slot \<noteq> src; slot = dest; src \<in> descendants_of p m \<or> p = src; m p = None; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 3. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> src; slot = dest; src \<in> descendants_of p m \<or> p = src; m p = None; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> src; slot = dest; src \<in> descendants_of p m \<or> p = src; m p = None; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> src; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>slot \<noteq> src; slot \<noteq> dest; \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> src; slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> src; slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p = dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot p. \<lbrakk>slot \<noteq> src; slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> src; slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> src; slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None
 2. \<And>slot p. \<lbrakk>slot \<noteq> src; slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> src; slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of (s_d_swap p src dest) m \<and> slot \<noteq> src \<and> slot \<noteq> dest \<or> slot \<in> (if src \<in> descendants_of (s_d_swap p src dest) m then {dest} else {}) \<or> slot \<in> (if dest \<in> descendants_of (s_d_swap p src dest) m then {src} else {}) \<or> p = slot) \<and> (if p = dest then if m src = Some dest then Some src else m src else if p = src then if m dest = Some src then Some dest else m dest else if m p = Some src then Some dest else if m p = Some dest then Some src else m p) = None proof (prove)
goal:
No subgoals!