theory Deterministic_AI

lemma (in mdb_empty_abs) finite_depth:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "finite_depth m \<Longrightarrow> finite_depth n" apply(simp add: finite_depth_def descendants) apply(rule allI) apply(simp add: n_def) apply(case_tac "slota=slot") apply(simp) apply(simp) apply(erule_tac x=slota in allE) apply(elim exE conjE) apply(case_tac "p=slot") apply(simp) apply(subgoal_tac "\<exists>a. m a = Some slot \<and>
               (slota \<in> descendants_of a m \<or> slota = a)") prefer 2 apply(simp add: descendants_of_def cdt_parent_defs) apply(drule tranclD) apply(elim exE conjE) apply(simp) apply(rule_tac x=z in exI) apply(simp) apply(drule rtranclD) apply(erule disjE) apply(simp) apply(simp) apply(erule exE) apply(rule_tac x=a in exI) apply(simp) apply(fastforce) apply(rule_tac x=p in exI) apply(simp) done

(* Proof state trace *)
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>slota. \<exists>p. (p = slot \<longrightarrow> slot = slota \<and> n slot = None) \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<and> slota \<noteq> slot \<or> p = slota) \<and> n p = None) proof (prove)
goal (1 subgoal):
 1. \<And>slota. \<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None \<Longrightarrow> \<exists>p. (p = slot \<longrightarrow> slot = slota \<and> n slot = None) \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<and> slota \<noteq> slot \<or> p = slota) \<and> n p = None) proof (prove)
goal (1 subgoal):
 1. \<And>slota. \<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> (p = slot \<longrightarrow> slot = slota) \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<and> slota \<noteq> slot \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> (p = slot \<longrightarrow> slot = slota) \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<and> slota \<noteq> slot \<or> p = slota) \<and> m p = None)) proof (prove)
goal (2 subgoals):
 1. \<And>slota. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slota = slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> (p = slot \<longrightarrow> slot = slota) \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<and> slota \<noteq> slot \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> (p = slot \<longrightarrow> slot = slota) \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<and> slota \<noteq> slot \<or> p = slota) \<and> m p = None))
 2. \<And>slota. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slota \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> (p = slot \<longrightarrow> slot = slota) \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<and> slota \<noteq> slot \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> (p = slot \<longrightarrow> slot = slota) \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<and> slota \<noteq> slot \<or> p = slota) \<and> m p = None)) proof (prove)
goal (1 subgoal):
 1. \<And>slota. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slota \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> (p = slot \<longrightarrow> slot = slota) \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<and> slota \<noteq> slot \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> (p = slot \<longrightarrow> slot = slota) \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<and> slota \<noteq> slot \<or> p = slota) \<and> m p = None)) proof (prove)
goal (1 subgoal):
 1. \<And>slota. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slota \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (1 subgoal):
 1. \<And>slota. \<lbrakk>slota \<noteq> slot; \<exists>p. (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (1 subgoal):
 1. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (2 subgoals):
 1. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p = slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (2 subgoals):
 1. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> slota \<in> descendants_of p m \<or> p = slota)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (3 subgoals):
 1. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; \<exists>a. m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> slota \<in> descendants_of p m \<or> p = slota)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot\<rbrakk> \<Longrightarrow> \<exists>a. m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)
 3. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (3 subgoals):
 1. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot\<rbrakk> \<Longrightarrow> \<exists>a. m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; \<exists>a. m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> slota \<in> descendants_of p m \<or> p = slota)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 3. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (3 subgoals):
 1. \<And>slota p. \<lbrakk>slota \<noteq> slot; (slot, slota) \<in> {(p, c). m c = Some p}\<^sup>+; m slot = None; p = slot\<rbrakk> \<Longrightarrow> \<exists>a. m a = Some slot \<and> ((a, slota) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> slota = a)
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; \<exists>a. m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> slota \<in> descendants_of p m \<or> p = slota)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 3. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (3 subgoals):
 1. \<And>slota p. \<lbrakk>slota \<noteq> slot; m slot = None; p = slot; \<exists>z. (slot, z) \<in> {(p, c). m c = Some p} \<and> (z, slota) \<in> {(p, c). m c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> \<exists>a. m a = Some slot \<and> ((a, slota) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> slota = a)
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; \<exists>a. m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> slota \<in> descendants_of p m \<or> p = slota)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 3. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (3 subgoals):
 1. \<And>slota p z. \<lbrakk>slota \<noteq> slot; m slot = None; p = slot; (slot, z) \<in> {(p, c). m c = Some p}; (z, slota) \<in> {(p, c). m c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> \<exists>a. m a = Some slot \<and> ((a, slota) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> slota = a)
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; \<exists>a. m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> slota \<in> descendants_of p m \<or> p = slota)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 3. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (3 subgoals):
 1. \<And>slota p z. \<lbrakk>slota \<noteq> slot; m slot = None; p = slot; m z = Some slot; (z, slota) \<in> {(p, c). m c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> \<exists>a. m a = Some slot \<and> ((a, slota) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> slota = a)
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; \<exists>a. m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> slota \<in> descendants_of p m \<or> p = slota)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 3. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (3 subgoals):
 1. \<And>slota p z. \<lbrakk>slota \<noteq> slot; m slot = None; p = slot; m z = Some slot; (z, slota) \<in> {(p, c). m c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> m z = Some slot \<and> ((z, slota) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> slota = z)
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; \<exists>a. m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> slota \<in> descendants_of p m \<or> p = slota)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 3. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (3 subgoals):
 1. \<And>slota p z. \<lbrakk>slota \<noteq> slot; m slot = None; p = slot; m z = Some slot; (z, slota) \<in> {(p, c). m c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> (z, slota) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> slota = z
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; \<exists>a. m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> slota \<in> descendants_of p m \<or> p = slota)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 3. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (3 subgoals):
 1. \<And>slota p z. \<lbrakk>slota \<noteq> slot; m slot = None; p = slot; m z = Some slot; z = slota \<or> z \<noteq> slota \<and> (z, slota) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (z, slota) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> slota = z
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; \<exists>a. m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> slota \<in> descendants_of p m \<or> p = slota)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 3. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (4 subgoals):
 1. \<And>slota p z. \<lbrakk>slota \<noteq> slot; m slot = None; p = slot; m z = Some slot; z = slota\<rbrakk> \<Longrightarrow> (z, slota) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> slota = z
 2. \<And>slota p z. \<lbrakk>slota \<noteq> slot; m slot = None; p = slot; m z = Some slot; z \<noteq> slota \<and> (z, slota) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (z, slota) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> slota = z
 3. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; \<exists>a. m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> slota \<in> descendants_of p m \<or> p = slota)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 4. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (3 subgoals):
 1. \<And>slota p z. \<lbrakk>slota \<noteq> slot; m slot = None; p = slot; m z = Some slot; z \<noteq> slota \<and> (z, slota) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (z, slota) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> slota = z
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; \<exists>a. m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> slota \<in> descendants_of p m \<or> p = slota)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 3. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (2 subgoals):
 1. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; \<exists>a. m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> slota \<in> descendants_of p m \<or> p = slota)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (2 subgoals):
 1. \<And>slota p a. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> slota \<in> descendants_of p m \<or> p = slota)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None))
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (2 subgoals):
 1. \<And>slota p a. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> (m a = Some slot \<longrightarrow> a \<noteq> slot \<and> (a \<noteq> slot \<longrightarrow> slota \<in> descendants_of a m \<or> a = slota)) \<and> (m a \<noteq> Some slot \<longrightarrow> a \<noteq> slot \<and> (a \<noteq> slot \<longrightarrow> (slota \<in> descendants_of a m \<or> a = slota) \<and> m a = None))
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (2 subgoals):
 1. \<And>slota p a. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of slot m; m slot = None; p = slot; m a = Some slot \<and> (slota \<in> descendants_of a m \<or> slota = a)\<rbrakk> \<Longrightarrow> a \<noteq> slot \<and> (a \<noteq> slot \<longrightarrow> slota \<in> descendants_of a m \<or> a = slota)
 2. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (1 subgoal):
 1. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>p. (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal (1 subgoal):
 1. \<And>slota p. \<lbrakk>slota \<noteq> slot; slota \<in> descendants_of p m \<or> p = slota; m p = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> (m p = Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m slot = None)) \<and> (m p \<noteq> Some slot \<longrightarrow> p \<noteq> slot \<and> (p \<noteq> slot \<longrightarrow> (slota \<in> descendants_of p m \<or> p = slota) \<and> m p = None)) proof (prove)
goal:
No subgoals!