theory Deterministic_AI

lemma finite_depth:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "finite_depth m'" apply (insert findepth) apply(simp add: finite_depth_def descendants) apply(rule allI) apply(case_tac "slot=dest") apply(erule_tac x=src in allE) apply(elim exE conjE) apply(erule disjE) apply(rule_tac x=p in exI) apply(simp add: m'_def m''_def) apply(rule conjI) apply(rule impI, simp add: dest_desc) apply(intro impI notI) apply(insert valid_mdb)[1] apply(drule_tac slot=src in desc_not_parent, simp add: m) apply(simp add: m'_def m''_def) apply(fastforce) apply(simp add: m'_def m''_def) apply(erule_tac x=slot in allE) apply(elim exE conjE) apply(case_tac "p=src") apply(erule disjE) apply(rule_tac x=dest in exI) apply(simp) apply(rule_tac x=src in exI) apply(simp) apply(case_tac "slot=src") apply(rule_tac x=src in exI) apply(simp) apply(rule_tac x=p in exI) apply(simp) apply(intro conjI impI) apply(simp add: dest_desc) apply(simp add: dest_desc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite_depth m' proof (prove)
goal (1 subgoal):
 1. finite_depth m \<Longrightarrow> finite_depth m' 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. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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 = dest\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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> dest\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m' p = None))) proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>slot = dest; \<exists>p. (src \<in> descendants_of p m \<or> p = src) \<and> m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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> dest\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m' p = None))) proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; src \<in> descendants_of p m \<or> p = src; m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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> dest\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m' p = None))) proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m p = None; src \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m' p = None)))
 2. \<And>slot p. \<lbrakk>slot = dest; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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> dest\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m' p = None))) proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m p = None; src \<in> descendants_of p m\<rbrakk> \<Longrightarrow> (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m' p = None)))
 2. \<And>slot p. \<lbrakk>slot = dest; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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> dest\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m' p = None))) proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m p = None; src \<in> descendants_of p m\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> m src = None) \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src)
 2. \<And>slot p. \<lbrakk>slot = dest; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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> dest\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m' p = None))) proof (prove)
goal (4 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m p = None; src \<in> descendants_of p m\<rbrakk> \<Longrightarrow> p = dest \<longrightarrow> m src = None
 2. \<And>slot p. \<lbrakk>slot = dest; m p = None; src \<in> descendants_of p m\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> p \<noteq> src
 3. \<And>slot p. \<lbrakk>slot = dest; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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> dest\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m' p = None))) proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m p = None; src \<in> descendants_of p m\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> p \<noteq> src
 2. \<And>slot p. \<lbrakk>slot = dest; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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> dest\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m' p = None))) proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m p = None; src \<in> descendants_of p m; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> False
 2. \<And>slot p. \<lbrakk>slot = dest; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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> dest\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m' p = None))) proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m p = None; src \<in> descendants_of p m; p \<noteq> dest; p = src; valid_mdb s\<rbrakk> \<Longrightarrow> False
 2. \<And>slot p. \<lbrakk>slot = dest; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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> dest\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m' p = None))) proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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> dest\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m' p = None))) proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot = dest; m src = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> p = dest) \<and> (m p \<noteq> Some src \<longrightarrow> (src \<in> descendants_of p m \<longrightarrow> p \<noteq> dest \<longrightarrow> p \<noteq> src \<and> (p \<noteq> src \<longrightarrow> m p = None)) \<and> (src \<notin> descendants_of p m \<longrightarrow> p = dest))
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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> dest\<rbrakk> \<Longrightarrow> \<exists>p. (src \<in> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> slot = dest \<or> p = slot) \<and> m' p = None))) \<and> (src \<notin> descendants_of p m \<longrightarrow> (p = dest \<longrightarrow> (slot \<in> descendants_of src m \<or> dest = slot) \<and> m' dest = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot \<and> m' src = None) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> 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> dest\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None))) proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>slot \<noteq> dest; \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None))) proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None))) proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p = src\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None)))
 2. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None))) proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; m p = None; p = src; slot \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None)))
 2. \<And>slot p. \<lbrakk>slot \<noteq> dest; m p = None; p = src; p = slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None)))
 3. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None))) proof (prove)
goal (3 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; m p = None; p = src; slot \<in> descendants_of p m\<rbrakk> \<Longrightarrow> (m dest = Some src \<longrightarrow> (dest = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (dest \<noteq> dest \<longrightarrow> (dest = src \<longrightarrow> src = slot) \<and> dest = src)) \<and> (m dest \<noteq> Some src \<longrightarrow> (dest = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (dest \<noteq> dest \<longrightarrow> (dest = src \<longrightarrow> src = slot) \<and> (dest \<noteq> src \<longrightarrow> (slot \<in> descendants_of dest m \<and> slot \<noteq> src \<or> dest = slot) \<and> m dest = None)))
 2. \<And>slot p. \<lbrakk>slot \<noteq> dest; m p = None; p = src; p = slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None)))
 3. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None))) proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; m p = None; p = src; p = slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None)))
 2. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None))) proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; m p = None; p = src; p = slot\<rbrakk> \<Longrightarrow> (m src = Some src \<longrightarrow> (src = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (src \<noteq> dest \<longrightarrow> (src = src \<longrightarrow> src = slot) \<and> src = src)) \<and> (m src \<noteq> Some src \<longrightarrow> (src = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (src \<noteq> dest \<longrightarrow> (src = src \<longrightarrow> src = slot) \<and> (src \<noteq> src \<longrightarrow> (slot \<in> descendants_of src m \<and> slot \<noteq> src \<or> src = slot) \<and> m src = None)))
 2. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None))) proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None))) proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src; slot = src\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None)))
 2. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src; slot \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None))) proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src; slot = src\<rbrakk> \<Longrightarrow> (m src = Some src \<longrightarrow> (src = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (src \<noteq> dest \<longrightarrow> (src = src \<longrightarrow> src = slot) \<and> src = src)) \<and> (m src \<noteq> Some src \<longrightarrow> (src = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (src \<noteq> dest \<longrightarrow> (src = src \<longrightarrow> src = slot) \<and> (src \<noteq> src \<longrightarrow> (slot \<in> descendants_of src m \<and> slot \<noteq> src \<or> src = slot) \<and> m src = None)))
 2. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src; slot \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None))) proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src; slot \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None))) proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src; slot \<noteq> src\<rbrakk> \<Longrightarrow> (m p = Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> p = src)) \<and> (m p \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src = slot) \<and> (p \<noteq> src \<longrightarrow> (slot \<in> descendants_of p m \<and> slot \<noteq> src \<or> p = slot) \<and> m p = None))) proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src; slot \<noteq> src\<rbrakk> \<Longrightarrow> p = dest \<longrightarrow> slot \<in> descendants_of src m \<and> m src = None proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src; slot \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> slot \<in> descendants_of src m
 2. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src; slot \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> m src = None proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; p \<noteq> src; slot \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> m src = None proof (prove)
goal:
No subgoals!